Document Open Access Logo

Minimisation of Models Satisfying CTL Formulas

Authors Serenella Cerrito, Amélie David, Valentin Goranko

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.13.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Serenella Cerrito
  • IBISC, Univ Evry, Université Paris-Saclay, 91025, Evry, France
Amélie David
  • IBISC, Univ Evry, Université Paris-Saclay, 91025, Evry, France
Valentin Goranko
  • Stockholm University, Sweden
  • University of Johannesburg (visiting professorship), South Africa

Funding

The work of Valentin Goranko was supported by a research grant 2015-04388 of the Swedish Research Council.

Cite AsGet BibTex

Serenella Cerrito, Amélie David, and Valentin Goranko. Minimisation of Models Satisfying CTL Formulas. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.13

Abstract

We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Computing methodologies → Temporal reasoning
Keywords
  • CTL
  • model minimisation
  • bisimulation reduction
  • tableaux-based reduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Adnan Aziz, Thomas Shiple, Vigyan Singhal, Robert Brayton, and Alberto Sangiovanni-Vincentelli. Formula-Dependent Equivalence for Compositional CTL Model Checking. Formal Methods in System Design, 21(2):193-224, 2002. Google Scholar
  2. A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18(3):247-269, 1992. Google Scholar
  3. Ahmed Bouajjani, Jean-Claude Fernandez, and Nicolas Halbwachs. Minimal Model Generation. In Proc of CAV '90, pages 197-203, 1990. Google Scholar
  4. Laura Bozzelli and David Pearce. On the Expressiveness of Temporal Equilibrium Logic. In Proc. of JELIA 2016, pages 159-173, 2016. Google Scholar
  5. Serenella Cerrito and Amélie David. Minimisation of ATL* Models. In Proc. of TABLEAUX 2017, pages 193-208, 2017. Google Scholar
  6. Massimiliano Chiodo, Thomas R. Shiple, Alberto L. Sangiovanni-Vincentelli, and Robert K. Brayton. Automatic compositional minimization in CTL model checking. In Proc. of ICCAD'1992, pages 172-178, 1992. Google Scholar
  7. E. Clarke and E.A. Emerson. Design and synthesis of synchronisation skeletons using branching time temporal logic. In Logics of Programs, pages 52-71. Springer, 1981. Google Scholar
  8. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
  9. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986. Google Scholar
  10. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science, volume 58 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, October 2016. URL: http://www.cambridge.org/9781107028364.
  11. V. Goranko and M. Otto. Model Theory of Modal Logic. In Handbook of Modal Logic, pages 249-330. Elsevier, 2007. Google Scholar
  12. Susanne Graf and Bernhard Steffen. Compositional minimization of finite state systems. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer-Aided Verification, pages 186-196, Berlin, Heidelberg, 1991. Springer. Google Scholar
  13. Paris C. Kanellakis and Scott A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86(1):43-68, 1990. Google Scholar
  14. Aceto L., Ingolfsdottir, and Jiri S. The Algorithmics of Bisimilarity. In Sangiorgi D. and Rutten J., editors, Advanced topics in bisimulation and coinduction, pages 100-171. Cambridge University Press, 2012. Google Scholar
  15. Fabio Mogavero and Aniello Murano. Branching-Time Temporal Logics with Minimal Model Quantifiers. In Developments in Language Theory, 13th International Conference, DLT 2009, Stuttgart, Germany, June 30 - July 3, 2009. Proceedings, pages 396-409, 2009. URL: https://doi.org/10.1007/978-3-642-02737-6_32.
  16. R. Paige and R.E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, 1987. Google Scholar
  17. Thomas R. Shiple, Massimiliano Chiodo, Alberto L. Sangiovanni-Vincentelli, and Robert K. Brayton. Automatic Reduction in CTL Compositional Model Checking. In Proc. of CAV'92, pages 234-247, 1992. Google Scholar
  18. Colin Stirling. Bisimulation and Logic. In Sangiorgi D. and Rutten J., editors, Advanced topics in bisimulation and coinduction, pages 173-195. Cambridge University Press, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact