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

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.

[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.

[3]

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

[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.

[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.

[6]

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

[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.

[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.

[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.

[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.

[11]

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

[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.

[13]

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

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[23]

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

[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.

[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.

[26]

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

[27]

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

[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.

[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.

[30]

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

[31]

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

[32]

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

[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.

[34]

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

[35]

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

[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.

[37]

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

[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.

[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.

[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.

[41]

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

Cited By

Das SSharma A(2025)Embeddings Between State and Action Based Probabilistic LogicsFormal Aspects of Computing10.1145/369643137:2(1-58)Online publication date: 3-Mar-2025
https://dl.acm.org/doi/10.1145/3696431
Bisping BJansen D(2024)One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace SemanticsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.6412(71-88)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.6
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
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

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

Copyright © 1995 ACM.

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

249
Total Citations
View Citations
1,717
Total Downloads

Downloads (Last 12 months)131
Downloads (Last 6 weeks)19

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Das SSharma A(2025)Embeddings Between State and Action Based Probabilistic LogicsFormal Aspects of Computing10.1145/369643137:2(1-58)Online publication date: 3-Mar-2025
https://dl.acm.org/doi/10.1145/3696431
Bisping BJansen D(2024)One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace SemanticsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.6412(71-88)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.6
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
Hendriks DOortwijn W(2024)gLTSdiff: a generalized framework for structural comparison of software behaviorSoftware and Systems Modeling10.1007/s10270-024-01239-0Online publication date: 28-Nov-2024
https://doi.org/10.1007/s10270-024-01239-0
Beneš NBrim LHuvar OPastva SŠafránek D(2024)Symbolic Model Checking of Hybrid CTL on Coloured Kripke StructuresAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_11(212-233)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-78750-8_11
Zouari SZiemiański KFahrenberg U(2024)Bisimulations and Logics for Higher-Dimensional AutomataTheoretical Aspects of Computing – ICTAC 202410.1007/978-3-031-77019-7_8(132-150)Online publication date: 25-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-77019-7_8
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
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents