Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2007: Automated Technology for Verification and Analysis pp 19–34Cite as

Branching vs. Linear Time: Semantical Perspective

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4762))

Abstract

The discussion in the computer-science literature of the relative merits of linear- versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that the linear-time framework is not expressive enough semantically, making linear-time logics lacking in expressiveness. In this work we examine the branching-linear issue from the perspective of process equivalence, which is one of the most fundamental notions in concurrency theory, as defining a notion of process equivalence essentially amounts to defining semantics for processes. Over the last three decades numerous notions of process equivalence have been proposed. Researchers in this area do not anymore try to identify the “right” notion of equivalence. Rather, focus has shifted to providing taxonomic frameworks, such as “the linear-branching spectrum”, for the many proposed notions and trying to determine suitability for different applications.

We revisit here this issue from a fresh perspective. We postulate three principles that we view as fundamental to any discussion of process equivalence. First, we borrow from research in denotational semantics and take observational equivalence as the primary notion of equivalence. This eliminates many testing scenarios as either too strong or too weea. Second, we require the description of a process to fully specify all relevant behavioral aspects of the process. Finally, we require observable process behavior to be reflected in its input/output behavior. Under these postulates the distinctions between the linear and branching semantics tend to evaporate. As an example, we apply these principles to the framework of transducers, a classical notion of state-based processes that dates back to the 1950s and is well suited to hardware modeling. We show that our postulates result in a unique notion of process equivalence, which is trace based, rather than tree based.

Work supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326, CCF-0613889, and ANI-0216467, by BSF grant 9800096, and by gift from Intel.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languagues and Systems 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. Abramsky, S.: Observation equivalence as a testing equivalence. Theor. Comput. Sci. 53, 225–241 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  3. Abramsky, S.: What are the fundamental structures of concurrency?: We still don’t know! Electr. Notes Theor. Comput. Sci. 162, 37–41 (2006)

    Article  Google Scholar 

  4. Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Beer, I., Ben-David, S., Geist, D., Gewirtzman, R., Yoeli, M.: Methodology and system for practical formal verification of reactive hardware. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 182–193. Springer, Heidelberg (1994)

    Google Scholar 

  6. Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  7. Berry, G., Gonthier, G.: The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming 19(2), 87–152 (1992)

    Article  MATH  Google Scholar 

  8. Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  9. Bloom, B., Meyer, A.R.: Experimenting with process equivalence. Theor. Comput. Sci. 101(2), 223–237 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  10. Bol, R.N., Groote, J.F.: The meaning of negative premises in transition system specifications. J. ACM 43(5), 863–914 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  11. Boreale, M., Pugliese, R.: Basic observables for processes. Information and Computation 149(1), 77–98 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  12. Brookes, S.D.: Traces, pomsets, fairness and full abstraction for communicating processes. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 466–482. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science 59, 115–131 (1988)

    Article  MathSciNet  Google Scholar 

  14. Carmo, J., Sernadas, A.: Branching vs linear logics yet again. Formal Aspects of Computing 2, 24–59 (1990)

    Article  Google Scholar 

  15. Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Databases, pp. 293–322. Plenum Press (1978)

    Google Scholar 

  16. Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  17. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languagues and Systems 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  18. Clarke, E.M., Grumberg, O., Long, D.: Verification tools for finite-state concurrent systems. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Decade of Concurrency – Reflections and Perspectives (Proceedings of REX School). LNCS, vol. 803, pp. 124–175. Springer, Heidelberg (1994)

    Google Scholar 

  19. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  20. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984)

    Article  MATH  Google Scholar 

  21. Dill, D.L.: Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, Cambridge (1989)

    Google Scholar 

  22. Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)

    Google Scholar 

  23. Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proc. 7th Int. Colloq. on Automata, Languages, and Programming, pp. 169–181 (1980)

    Google Scholar 

  24. Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: On branching versus linear time. Journal of the ACM 33(1), 151–178 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  25. Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time logic strikes back. In: Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 84–96 (1985)

    Google Scholar 

  26. Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 136–145. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  27. Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Formal Methods in System Design 21(1), 39–78 (2002)

    Article  MATH  Google Scholar 

  28. van Glabbeek, R.J.: The linear time – branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra. Ch-1, pp. 3–99. Elsevier, Amsterdam (2001)

    Google Scholar 

  29. Goering, R.: Model checking expands verification’s scope. Electronic Engineering Today (February 1997)

    Google Scholar 

  30. Groote, J.F.: Transition system specifications with negative premises. Theor. Comput. Sci. 118(2), 263–299 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  31. Hachtel, G.D., Somenzi, F.: Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, Dordrecht (1996)

    MATH  Google Scholar 

  32. Hartmanis, J., Stearns, R.E.: Algebraic Structure Theory of Sequential Machines. Prentice-Hall, Englewood Cliffs (1966)

    MATH  Google Scholar 

  33. Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)

    MATH  Google Scholar 

  34. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  35. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  36. Jonsson, B.: A fully abstract trace model for dataflow networks. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 155–165 (1989)

    Google Scholar 

  37. Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 406–419. Springer, Heidelberg (2007)

    Google Scholar 

  38. Lamport, L.: Sometimes is sometimes not never - on the temporal logic of programs. In: Proc. 7th ACM Symp. on Principles of Programming Languages, pp. 174–185 (1980)

    Google Scholar 

  39. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 97–107 (1985)

    Google Scholar 

  40. Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)

    MATH  MathSciNet  Google Scholar 

  41. Main, M.G.: Trace, failure and testing equivalences for communicating processes. Int’l J. of Parallel Programming 16(5), 383–400 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  42. Marek, W.W., Trusczynski, M.: Nonmonotonic Logic: Context-Dependent Reasoning. Springer, Heidelberg (1997)

    Google Scholar 

  43. McCarthy, J.: Circumscription - a form of non-monotonic reasoning. Artif. Intell. 13(1-2), 27–39 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  44. Milner, R.: Processes: a mathematical model of computing agents. In: Logic Colloquium, North Holland, pp. 157–173 (1975)

    Google Scholar 

  45. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Google Scholar 

  46. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  47. Olderog, E.R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. Acta Inf. 23(1), 9–66 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  48. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Theoretical Computer Science, GI 1981. LNCS, vol. 104, Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  49. Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  50. Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985)

    Google Scholar 

  51. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Proc. 8th ACM Symp. on Principles of Programming Languages. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)

    Google Scholar 

  52. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal of the ACM 32, 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  53. Stirling, C.: Comparing linear and branching time temporal logics. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 1–20. Springer, Heidelberg (1989)

    Google Scholar 

  54. Stirling, C.: The joys of bisimulation. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 142–151. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  55. Vaandrager, F.W.: On the relationship between process algebra and input/output automata. In: Proc. 6th IEEE Symp. on Logic in Computer Science, pp. 387–398 (1991)

    Google Scholar 

  56. Vardi, M.Y.: Linear vs. branching time: A complexity-theoretic perspective. In: Proc. 13th IEEE Sym. on Logic in Computer Science, pp. 394–405 (1998)

    Google Scholar 

  57. Vardi, M.Y.: Sometimes and not never re-revisited: on branching vs. linear time. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 1–17. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  58. Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  59. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st IEEE Symp. on Logic in Computer Science, pp. 332–344 (1986)

    Google Scholar 

  60. Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)

    Google Scholar 

  61. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rice University, Department of Computer Science, Houston, TX 77005-1892, USA

    Sumit Nain & Moshe Y. Vardi

Authors
  1. Sumit Nain
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Kedar S. Namjoshi Tomohiro Yoneda Teruo Higashino Yoshio Okamura

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nain, S., Vardi, M.Y. (2007). Branching vs. Linear Time: Semantical Perspective. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds) Automated Technology for Verification and Analysis. ATVA 2007. Lecture Notes in Computer Science, vol 4762. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75596-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-75596-8_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-75595-1

  • Online ISBN: 978-3-540-75596-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation