article

Free access

Three logics for branching bisimulation

Authors:

Rocco De Nicola,

Frits VaandragerAuthors Info & Claims

Journal of the ACM (JACM), Volume 42, Issue 2

Pages 458 - 487

https://doi.org/10.1145/201019.201032

Published: 01 March 1995 Publication History

PDF eReader

Abstract

Three temporal logics are introduced that induce on labeled transition systems the same identifications as branching bisimulation, a behavioral equivalence that aims at ignoring invisible transitions while preserving the branching structure of systems. The first logic is an extension of Hennessy-Milner Logic with an “until” operator. The second one is another extension of Hennessy-Milner Logic, which exploits the power of backward modalities. The third logic is CTL* without the next-time operator. A relevant side-effect of the last characterization is that it sets a bridge between the state- and action-based approaches to the semantics of concurrent systems.

References

[1]

~ABRAMSKY, S. 1989. Observation equivalence as a testing equivalence. Theoret. Comput. Scz. 53, ~225-241.

Crossref

Google Scholar

[2]

~AKKERMAN, G. J., AND BAETEN, J. C. M. 1990. Term rewriting analysis in process algebra. ~Report P9006. Programming Research Group, Univ. Amsterdam, Amsterdam, the Netherlands.

Google Scholar

[3]

~BAETEN, J. C. M. 1990. Applications of process algebra. Cambridge Tract in Theoretical ~Computer Science, Vol. 17. Cambridge University Press, Cambridge, England.

Crossref

Google Scholar

[4]

~BAETEN, J. C. M., AND WEIJLAND, W. P. 1990. Process Algebra. Cambridge Tract in Theoretical ~Computer Science, Vol. 18. Cambridge University Press, Cambridge England.

Crossref

Google Scholar

[5]

~BLOOM, B., ISTRAIL, S., .AND MEYER, A. R. 1988/1990. Bisimulation can't be traced: Preliminary ~report. In Conference Record of the 15th ACM Sympostum on Principles of Programming ~Languages (POPL) (San Diego, Calif.), ACM, New York, pp. 229-239. Full version appeared as ~Tech. Rep. TR 90-1150, Cornell Univ., Ithaca, N.Y., 1990.

Crossref

Google Scholar

[6]

~BOLOGNESI, T., VAN DE LANGMAAT, J. AND ViSSERS, C. 1995. Lotosphere: software development ~with LOTUS, Kluver Dordrect.

Crossref

Google Scholar

[7]

~BROWNE, M. C., CLARKE, E. M., AND GROMBERG, O. 1988. Characterizing finite Kripke struc- ~tures in propositional temporal logic. Theoret. Comput. Scl. 59, 1, 2, 115-131.

Crossref

Google Scholar

[8]

~CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite state ~concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Syst. 8, 2 ~(Apr.), 244-263.

Crossref

Google Scholar

[9]

~CLARKE, E. M., LONG, D. E., AND MACMILLAN, K. L. 1989. Compositional model checking. In ~Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS) (Asilomar, ~Calif.). IEEE Computer Society Press, Washington, D.C., pp. 353-362.

Crossref

Google Scholar

[10]

~CLEAVELAND, R., PARROW, J., AND STEFFEN, B. 1990. The concurrency workbench. In Automatic ~Verification Methods for Fmzte State Systems J. Sifakis, ed. Lecture Notes in Computer Science, ~vol. 407. Springer-Verlag, New York, pp. 24-37.

Crossref

Google Scholar

[11]

~DARONDEAU, PH., AND DEGANO, P. 1991. About semantic action refinement. Fund. b~f. XIV, 2, ~221-234.

Crossref

Google Scholar

[12]

~DE BAKKER, J., DE ROEVER, W. P., AND ROZENBERG, G. EDS. 1989. Linear time, branching time ~and partial order in logics and models for concurrency. In Lecture Notes in Computer Science, ~vol. 354, Springer-Verlag, New York.

Google Scholar

[13]

~DE NICOLA, R. 1987. Extensional eqmvalences for transition systems. Acta Inf. 24, 211-237.

Crossref

Google Scholar

[14]

~DE NICOLA, R., FANTECHI, A., GNESI, S., AND RISTORI, G. 1993. An action-based framework for ~verifying logical and behavioral properties of concurrent systems. Comput. Nero,. and ISDN ~Svst. 25, 761-778.

Crossref

Google Scholar

[15]

~DE NICOLA, R., INVERARDI, P., AND NESI, M. 1990a. Using axiomatic presentation of behavioural ~equivalences for manipulating CCS specifications. In Automatic Verificatton Methods for Fimte ~State Systems (Slfakis, ed.). Lecture Notes in Computer Science, Vol. 407. Springer-Verlag, New ~York, pp. 54-67.

Crossref

Google Scholar

[16]

~DE NICOL^, R., MONT~,NARI, U., AND VAANDRAGER, F. W. 1990b. Back and Forth Bis~mulations. ~In CONCUR '90, J. Baeten, and J. W. Klop, eds. Lecture Notes in Computer Science, vol. 458. ~Springer-Verlag, New York, pp. 152-165.

Crossref

Google Scholar

[17]

~DE NICOLA, R., AND VAANDRAGER, F. W. 1990a. Action versus state based logics for transition ~systems. In Semantics of Concurrency, I. Guessanan, ed. Lecture Notes in Computer Science, ~vol. 469. Sprmger-Verlag, New York, pp. 407-419.

Crossref

Google Scholar

[18]

~DE NICOLA, R., AND VAANDRAGER, F. W. 1990b. Three logics for branching bisimulation ~(Extended Abstract). In Proceedings of the 5th Annual Symposium on Logzc zn Computer Scie~zce ~(LICS). IEEE Computer Society Press, New York, pp. 118 129.

Google Scholar

[19]

~EMERSON, E. A., AND HALPERN, J. Y. 1986. "Sometimes" and "Not Never" Rewsited: On ~branching versus linear time temporal logic. J. ACM 33, 1 (Jan.) 151-178.

Crossref

Google Scholar

[20]

~EMERSON, E. A., AND LH, C. L. 1984. Model checking under generalized fairness constraints. ~Technical Report TR-84-20, Dept. of Computer Sciences, University of Texas at Austin, Austin, ~Texas, June.

Crossref

Google Scholar

[21]

~EMERSON, E. m., AND SRINIVASAN, J. 1989. Branching time temporal logic. In Linear Ttme, ~Branching Ttme and Pamal Order in Logics and Models for Concurrency, J. de Bakker, W. P. de ~Roever, and G. Rozenberg, Eds Lecture Notes in Computer Science, voI. 354. Springer-Verlag, ~New York, pp. 123-172.

Crossref

Google Scholar

[22]

~GROOTE, J. F., AND VAANDRAGER, F. W. 1990. An efficient algonthm for branching blsimulat~on ~and stuttering equivalence. In Proceedings oflCALP '90, M. S. Paterson, Ed. Lecture Notes in ~Computer Science, vol. 443. Springer-Verlag, New York, pp. 626-638.

Crossref

Google Scholar

[23]

~VAN GLABBEEK, R. J. 1990. Comparative concurrency semantics and refinement of actions. ~Ph.D. dissertation, Free University, Amsterdam, The Netherlands.

Google Scholar

[24]

~VAN GLABBEEK, R. J., AND WEIJLAND, W. P. 1989/1991. Branching time and abstraction in ~bisimulation semantics (extended abstract). In Information Processing '89, G. X. Ritter, ed. ~North Holland, Amsterdam, The Netherlands, pp. 613-618. Full paper appeared as CWI ~Report CS-R9120, Amsterdam 1991.

Google Scholar

[25]

~VAN GLABBEEK, R. J., AND WEIJLAND, W. P. 1989. Refinement in branching time semantics. In ~Proceedings of the AMAST Conference. IOWA pp. 197-201.

Google Scholar

[26]

~HENNESSY, M., AND MILNER, R. 1985. Algebraic laws for nondeterminism and concurrency. J. ~ACM 32, 1 (Jan.). 137-161.

Crossref

Google Scholar

[27]

~HENNESSY, M., AND STIRLING, C. 1985. The power of the future perfect in program logics. Inf. ~Control 67, 23-52.

Crossref

Google Scholar

[28]

~JONSSON, B., KHAN, A. H., AND PARROW, J. 1990. Implementing a model checking algorithm by ~adapting existing automated tools. In Automatic Verification Methods for Finite State Systems (J. ~Sifakis, ed.). Lecture Notes in Computer Science, vol. 407, Springer-Verlag, New York, pp. ~179-188.

Crossref

Google Scholar

[29]

~KORVER, H. 1992. Computing distinguishing formulae for branching bisimulation. In Proceed- ~ings of Computer Aided Verification, K. Larsen, and A. Skou, eds. Lecture Notes in Computer ~Science, vol. 575. Springer-Verlag, New York, pp. 13-23.

Crossref

Google Scholar

[30]

~KOUTNY, M. 1991. Axiom system induced by CTL* logic, 1990. Fund. bzf. XIV 2, 235-252.

Crossref

Google Scholar

[31]

~KOZEN, D. 1983. Results on the propositional mu-calculus. Theoret. Comput. Sci., 27, 333-354.

Google Scholar

[32]

~LAROUSSINE, F., PINCHINAT, S., AND SCHNOEBELEN, PH. 1995. Translation results for modal logics ~of reactive systems. Theoret. Comput. Sci. 140, 1, 53-71.

Crossref

Google Scholar

[33]

~LICHTENSTEIN, O., PNUELI, m., AND mUCK, L 1985. The glory of the past. In Proceedings of the ~Conference in Logics of Programs. Lecture Notes in Computer Science, vol. 193. Springer-Verlag, ~New York, pp. 196-218.

Crossref

Google Scholar

[34]

MILNER, R. 1989. Commumcation and Concurrency. Prentice-Hall, Englewood Cliffs, N.J.

Crossref

Google Scholar

[35]

MANNA, Z., AND PNUELI, A. 1992. The Temporal Logtc of Reactive and Concurrent Systems. ~Springer-Verlag, New York.

Crossref

Google Scholar

[36]

~PARK, D. M. R. 1989. Concurrency and automata on infinite sequences. In Proceedings of the 5th ~GI Conference (P. Deussen, ed.). Lecture Notes in Computer Science, vol. 104. Springer-Verlag, ~New York, pp. 167-183.

Crossref

Google Scholar

[37]

~OL~, E. E. 1992. An efficient implementation of branching bisimulation and distinguishing ~formulae. Master Thesis. Programming Research Group. Univ. Amsterdam, Amsterdam, The ~Netherlands.

Google Scholar

[38]

~PRATT, V. 1981. A decidable mu-calculus. In Proceedings of the 22nd Symposium on Foundations ~of Computer Science. IEEE Computer Society Press, New York, pp. 421-427.

Google Scholar

[39]

~STIRLING, C. 1989. Temporal logics for CCS. In Linear Time, Branching Time and Partial Order ~in Logics and Models for Concurrency, J. de Bakker, W. P. de Roever, and G. Rozenberg, eds. ~Lecture Notes in Computer Science, vol. 354. Springer-Verlag, New York, pp. 660-672.

Crossref

Google Scholar

[40]

~STmLING, C. 1992. Modal and temporal logics. In Handbook of Logic in Computer Science, vol. I ~(S. Abramsky, D. M. Gabbay and T. S. E. Maibaum, eds.) O. U. P., Oxford, pp. 477-563.

Crossref

Google Scholar

[41]

~STREET, R. S. 1982. Propositional dynamic logic of looping and converse is elementarily ~decidable. Inf. Cont. 54, 121-141.

Google Scholar

Cited By

View all

Das SSharma AHong JPark J(2024)A Formal Framework of Model and Logical Embeddings for Verification of Stochastic SystemsProceedings of the 39th ACM/SIGAPP Symposium on Applied Computing10.1145/3605098.3636032(1712-1721)Online publication date: 8-Apr-2024
https://dl.acm.org/doi/10.1145/3605098.3636032
Lennartson B(2024)Unified and Simplified BisimulationIFAC-PapersOnLine10.1016/j.ifacol.2024.07.03858:1(222-227)Online publication date: 2024
https://doi.org/10.1016/j.ifacol.2024.07.038
Bottoni PLabella APerelli G(2024)Strategies in Spatio-Temporal Logics for Multi-agent SystemsLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_18(287-305)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_18
Show More Cited By

Index Terms

Three logics for branching bisimulation
1. Theory of computation

Recommendations

Branching time and abstraction in bisimulation semantics

In comparative concurrency semantics, one usually distinguishes between linear time and branching time semantic equivalences. Milner's notion of observatin equivalence is often mentioned as the standard example of a branching time equivalence. In this ...
Bisimulation quantified logics: undecidability
FSTTCS '05: Proceedings of the 25th international conference on Foundations of Software Technology and Theoretical Computer Science

In this paper we introduce a general semantic interpretation for propositional quantification in all multi-modal logics based on bisimulations (bisimulation quantification). Bisimulation quantification has previously been considered in the context of ...
Intuitionistic counterparts of finitely-valued logics
ISMVL '96: Proceedings of the 26th International Symposium on Multiple-Valued Logic

We investigate the relation between Kripke's model structures for intuitionistic logic and the simple syntactical restriction that turns the classical sequent calculus into an intuitionistic one. For this purpose we generalize ordinary Kripke structures ...

Reviews

Reviewer: Fatma Mili

The operational semantics of concurrent systems are usually expressed in terms of labeled transition systems (such as finite state automata). Operational semantics are generally too detailed for an abstract analysis of a system. In particular, they are too detailed to naturally exhibit similarity between systems. Two concurrent systems are called “bisimulation equivalent” if they exhibit the same observed behavior. In this paper, the authors explore logic-based semantics. Logic semantics provide for a more abstract representation, and allow the expression of specific properties of a system without having to fully define it. The logics defined are interpreted over labeled transition graphs. For each logic introduced, the authors provide an equivalence relation and show that it precisely expresses bisimulation equivalence. The three logics introduced are two variations of the Hensley-Milner logic (HML) and a variation on the computation tree logic (CTL). The variations on the HML are interpreted over arc-labeled systems; the CTL is interpreted over state-labeled systems. Transformations are introduced to translate from one representation to the other (under some restrictive conditions). The paper has a three-page motivational introduction, and a page-and-a-half conclusion. The rest is mostly definitions, theorems, and proofs. The paper is worth the effort necessary to read it, but would certainly benefit from more commentary and explanations.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Journal of the ACM Volume 42, Issue 2

March 1995

250 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/201019

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 1995

Published in JACM Volume 42, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

244
Total Citations
View Citations
1,655
Total Downloads

Downloads (Last 12 months)104
Downloads (Last 6 weeks)9

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Das SSharma AHong JPark J(2024)A Formal Framework of Model and Logical Embeddings for Verification of Stochastic SystemsProceedings of the 39th ACM/SIGAPP Symposium on Applied Computing10.1145/3605098.3636032(1712-1721)Online publication date: 8-Apr-2024
https://dl.acm.org/doi/10.1145/3605098.3636032
Lennartson B(2024)Unified and Simplified BisimulationIFAC-PapersOnLine10.1016/j.ifacol.2024.07.03858:1(222-227)Online publication date: 2024
https://doi.org/10.1016/j.ifacol.2024.07.038
Bottoni PLabella APerelli G(2024)Strategies in Spatio-Temporal Logics for Multi-agent SystemsLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_18(287-305)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_18
Priser GVanneaux EFrehse G(2024)Robust Deterministic Abstractions for Supervising Discrete-Time Continuous SystemsReachability Problems10.1007/978-3-031-72621-7_13(187-202)Online publication date: 25-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72621-7_13
Abate AGiacobbe MSchnitzer Y(2024)Bisimulation LearningComputer Aided Verification10.1007/978-3-031-65633-0_8(161-183)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_8
Martens JGroote J(2024)Minimal Depth Distinguishing Formulas Without Until for Branching BisimulationLogics and Type Systems in Theory and Practice10.1007/978-3-031-61716-4_12(188-202)Online publication date: 22-May-2024
https://doi.org/10.1007/978-3-031-61716-4_12
Bernardo MEsposito A(2023)Modal Logic Characterizations of Forward, Reverse, and Forward-Reverse BisimilaritiesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.390.5390(67-81)Online publication date: 30-Sep-2023
https://doi.org/10.4204/EPTCS.390.5
Hendriks DOortwijn W(2023)gLTSdiff: A Generalized Framework for Structural Comparison of Software Behavior2023 ACM/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS)10.1109/MODELS58315.2023.00025(285-295)Online publication date: 1-Oct-2023
https://doi.org/10.1109/MODELS58315.2023.00025
Horne RMauw SYurkov S(2023)When privacy fails, a formula describes an attackTheoretical Computer Science10.1016/j.tcs.2023.113842959:COnline publication date: 30-May-2023
https://dl.acm.org/doi/10.1016/j.tcs.2023.113842
van Glabbeek R(2023)Modelling mutual exclusion in a process algebra with time-outsInformation and Computation10.1016/j.ic.2023.105079294(105079)Online publication date: Oct-2023
https://doi.org/10.1016/j.ic.2023.105079
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Branching time and abstraction in bisimulation semantics

Bisimulation quantified logics: undecidability

Intuitionistic counterparts of finitely-valued logics

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations