Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Model checking for action-based logics

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

A model checker is described that supports proving logical properties of concurrent systems. The logical properties can be described in different action-based logics (variants of Hennessy-Milner logic). The tools is based on the EMC model checker for the logic CTL. It therefore employs a set of translation functions from the considered logics to CTL, as well as a model translation function from labeled transition systems (models of the action-based logics) to Kripke structures (models for CTL). The obtained tool performs model checking in linear time complexity, and its correctness is guaranteed by the proof that the set of translation functions, coupled with the model translation function, preserves satisfiability of logical formulae.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. E.A. Emerson, and J. Halpern. “Sometime” and “not never” revisited: On branching versus linear time temporal logic.Journal of ACM, 33(1): pp. 151–178, January 1986.

    Google Scholar 

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

    Google Scholar 

  3. Z. Manna and A. Pnueli. The anchored version of the temporal framework. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency, J. de Bakker, P. de Roever, and G. Rozenberg (eds.).Lecture Notes in Computer Science, 354: 201–284, 1989.

  4. M.C. Browne, E.M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic.Theoretical Computer, Science, 59: 115–131, 1988.

    Google Scholar 

  5. E.A. Emerson and J. Srinivasan. Branching time temporal logic. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency, J. de Bakker, P. de Roever, and G. Rozenberg (eds.)Lecture Notes in Computer Science, 354: 123–172, 1989.

  6. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2): 244–263, April 1986.

    Google Scholar 

  7. A. Boujani, S. Graf, and J. Sifakis: A logic for the description of behaviors and properties of concurrent systems. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency, J. de Bakker, P. de Roever, and G. Rozenberg, (eds.).Lecture Notes in Computer Science 354: 398–410, 1989.

  8. C. Stirling. An introduction to modal and temporal logics for CCS. InConcurrency: Theory, Language, and Architecture, A. Yonezawa and T. Ito (eds.).Lecture Notes in Computer Science, 491: 2–20, 1990.

  9. R. De Nicola and F. Vaandrager. Three logics for branching bisimulations.Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS ′90) Philadelphia, PA, June, 1990. IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 118–129. To appear also inJournal of ACM.

    Google Scholar 

  10. R. De Nicola and F. Vaandrager. Action versus state based logics for transition systems.Proceedings Ecole de Printemps on Semantics of Concurrency, April 1990, I. Guessarian (ed.).Lecture Notes in Computer Science, 469: 407–419, 1990.

  11. K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion.Theoretical Computer Science, 72(2): 265–288, 1990.

    Google Scholar 

  12. R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. InAutomatic Verification Methods for Finite State Systems, J. Sifakis (ed.).Lecture Notes in Computer Science, 407: 24–37, 1990.

  13. R. Cleaveland, and B. Steffen. A linear-time model checking algorithm, for the alternation free modal mu-calculus.Formal Methods in System Design, 2: 121–147, 1993.

    Google Scholar 

  14. D. Park. Concurrency and automata on infinite sequences.Proceedings 5th GI Conference. Lecture Notes in Computer Science 104: 167–183, 1981.

    Google Scholar 

  15. R. Milner. A calculus of communicating systems.Lecture Notes in Computer Science, 92, 1980.

  16. R. Milner. Calculi for synchrony and asynchrony.Theoretical Computer Science, 25(3): 267–310, 1983.

    Google Scholar 

  17. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. InInformation Processing ′89, G.X. Ritter (ed.). North Holland, Amsterdam, 1989, pp. 613–618.

    Google Scholar 

  18. B. Jonsson, A.H. Khan and J. Parrow. Implementing a model checking algorithm, by adapting existing automated tools. InAutomatic Verification Methods for Finite State Systems, J. Sifakis (ed.). Lecture Notes in Computer Science, 407: 179–188, 1990.

  19. R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action-based framework for verifying logical and behavioral properties of concurrent systems.Computer Networks and ISDN Systems, 25: 761–778, 1993.

    Google Scholar 

  20. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond.Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS ′90), Philadelphia, USA, June 1990 IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 428–439.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Ingegneria della Informazione, Università degli Studi di Pisa, Via Diotisalvi 2, 156126, Pisa, Italy

    Alessandro Fantechi

  2. Istituto di Elaborazione, della Informazione del CNR, Via S Maria 46, I56126, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Informatica, Università degli Studi di Pisa, Corso Italia 40, I56125, Pisa, Italy

    Gioia Ristori

Authors
  1. Alessandro Fantechi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefania Gnesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gioia Ristori
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Fantechi, A., Gnesi, S. & Ristori, G. Model checking for action-based logics. Form Method Syst Des 4, 187–203 (1994). https://doi.org/10.1007/BF01384084

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01384084

Keywords

Search

Navigation