Skip to main content
SpringerLink
Log in

Safe Reasoning with Logic LTS

  • Conference paper
Book cover SOFSEM 2009: Theory and Practice of Computer Science (SOFSEM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5404))

Abstract

Previous work has introduced the setting of Logic LTS, together with a variant of ready simulation as fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator as well as the propositional connectives conjunction and disjunction. In this paper, we show how a temporal logic for specifying safety properties may be embedded into Logic LTS so that (a) the temporal operators are compositional for ready simulation and (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic’s satisfaction relation. The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated via a simple example.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Plotkin, G.: A logical view of composition. TCS 114(1), 3–30 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bloom, B.: Ready Simulation, Bisimulation, and the Semantics of CCS-like Languages. PhD thesis, MIT (1990)

    Google Scholar 

  3. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  4. De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  5. Fecher, H., Grabe, I.: Finite abstract models for deterministic transition systems. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 1–16. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. van Glabbeek, R.: The linear time – branching time spectrum II (1993), http://theory.stanford.edu/~rvg/abstracts.html#26

  7. Guerra, H., Costa, J.F.: Processes with local and global liveness requirements. J. of Logic and Algebraic Programming (to appear, 2008)

    Google Scholar 

  8. Henzinger, T.A., Rajamani, S.K.: Fair bisimulation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 299–314. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  10. Hoare, C.A.R., Jifeng, H.: Unif. Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  11. Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  12. Lamport, L.: The temporal logic of actions. TOPLAS 16(3), 872–923 (1994)

    Article  Google Scholar 

  13. Lüttgen, G., Vogler, W.: Conjunction on processes: Full-abstraction via ready-tree semantics. TCS 373(1–2), 19–40 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  14. Lüttgen, G., Vogler, W.: Ready simulation for concurrency: It’s logical? In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 752–763. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Lüttgen, G., Vogler, W.: Safe reasoning with Logic LTS. Technical report, Comp. Sci. Inst., Univ. of Augsburg, Germany (to appear, 2008)

    Google Scholar 

  16. Olderog, E.-R.: Nets, Terms and Formulas. Cambridge Tracts in Theoretical Computer Science, vol. 23. Cambridge Univ. Press, Cambridge (1991)

    Book  MATH  Google Scholar 

  17. Puhakka, A., Valmari, A.: Liveness and fairness in process-algebraic verification. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 202–217. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Raclet, J.-B.: Residual for component specifications. In: Formal Aspects of Component Software. ENTCS, vol. 215. Elsevier, Amsterdam (2008)

    Google Scholar 

  19. Ulidowski, I.: Refusal simulation and interactive games. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 208–222. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, YO10 5DD, U.K.

    Gerald Lüttgen

  2. Institut für Informatik, Universität Augsburg, D–86135, Augsburg, Germany

    Walter Vogler

Authors
  1. Gerald Lüttgen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Walter Vogler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Aarhus Graduate School of Science, University of Aarhus, Ny Munkegade Bldg 1521-110, DK-8000, Aarhus C, Denmark

    Mogens Nielsen

  2. Faculty of Informatics, Masaryk University, Botanická 68a, 60200, Brno, Czech Republic

    Antonín Kučera

  3. Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200, Aarhus N., Denmark

    Peter Bro Miltersen

  4. Ecole Polytechnique, Rue de Saclay, 91128, Palaiseau Cedex, France

    Catuscia Palamidessi  & Frank Valencia  & 

  5. Faculty of Mathematics and Physics, Charles University, Malostranské námestí 25, 118 00, Prague 1, Malá Strana, Czech Republic

    Petr Tůma

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lüttgen, G., Vogler, W. (2009). Safe Reasoning with Logic LTS. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-95891-8_35

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation