Document Open Access Logo

Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach

Authors Serenella Cerrito , Valentin Goranko , Sophie Paillocher

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.23.pdf
  • Filesize: 0.79 MB
  • 21 pages

Document Identifiers

Author Details

Serenella Cerrito
  • Université Paris Saclay, Univ EVRY, France
Valentin Goranko
  • Stockholm University, Sweden
  • and University of the Witwatersrand, Johannesburg, South Africa (visiting professorship)
Sophie Paillocher
  • Université Paris Saclay Univ EVRY, France

Acknowledgements

We thank the anonymous reviewers for their detailed and helpful comments.

Cite AsGet BibTex

Serenella Cerrito, Valentin Goranko, and Sophie Paillocher. Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.23

Abstract

In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • Linear temporal logic LTL
  • partial transition systems
  • partial model checking
  • partial model synthesis
  • tableaux

Metrics

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

References

  1. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. Google Scholar
  2. Henrik Reif Andersen. Partial model checking (extended abstract). In Proc. of LICS 1995, pages 398-407. IEEE Computer Society, 1995. Google Scholar
  3. Henrik Reif Andersen and Jørn Lind-Nielsen. Partial model checking of modal equations: A survey. Intern. J. on Software Tools for Technology Transfer, 2(3):242-259, 1999. Google Scholar
  4. Carlos Areces, Raul Fervari, and Guillaume Hoffmann. Relation-changing modal operators. Logic Journal of the IGPL, 23(4):601-627, 2015. Google Scholar
  5. Carlos Areces, Raul Fervari, Guillaume Hoffmann, and Mauricio Martel. Undecidability of relation-changing modal logics. In Proc. of DALI 2017, volume 10669 of LNCS, pages 1-16. Springer, 2017. Google Scholar
  6. Carlos Areces, Raul Fervari, Guillaume Hoffmann, and Mauricio Martel. Satisfiability for relation-changing logics. J. Log. Comput., 28(7):1443-1470, 2018. Google Scholar
  7. Guillaume Aucher, Philippe Balbiani, Luis Fariñas del Cerro, and Andreas Herzig. Global and local graph modifiers. Electr. Notes Theor. Comput. Sci., 231:293-307, 2009. Google Scholar
  8. Guillaume Aucher, Johan van Benthem, and Davide Grossi. Modal logics of sabotage revisited. J. Log. Comput., 28(2):269-303, 2018. Google Scholar
  9. Glenn Bruns and Patrice Godefroid. Generalized model checking: Reasoning about partial state spaces. In Catuscia Palamidessi, editor, CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science, pages 168-182. Springer, 2000. URL: https://doi.org/10.1007/3-540-44618-4_14.
  10. Gabriele Costa, David A. Basin, Chiara Bodei, Pierpaolo Degano, and Letterio Galletta. From natural projection to partial model checking and back. In Proc. of TACAS 2018, volume 10805 of LNCS, pages 344-361. Springer, 2018. Google Scholar
  11. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781139236119.
  12. Dov M. Gabbay. Reactive Kripke Semantics. Cognitive Technologies. Springer, 2013. Google Scholar
  13. Patrice Godefroid and Nir Piterman. LTL generalized model checking revisited. In Neil D. Jones and Markus Müller-Olm, editors, Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings, volume 5403 of Lecture Notes in Computer Science, pages 89-104. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-93900-9_11.
  14. Valentin Goranko. Model checking and model synthesis from partial models: a logic-based perspective. https://arxiv.org/abs/2012.12398, 2020. Google Scholar
  15. Orna Kupferman and Moshe Y. Vardi. Synthesis with incomplete informatio. In Howard Barringer, Michael Fisher, Dov Gabbay, and Graham Gough, editors, 2nd Intern. Conf. on Advances in Temporal Logic, pages 109-127, Dordrecht, 2000. Springer Netherlands. Google Scholar
  16. David A Schmidt. Binary relations for abstraction and refinement. In Workshop on Refinement and Abstraction, Amagasaki, Japan. Citeseer, 1999. Google Scholar
  17. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, July 1985. URL: https://doi.org/10.1145/3828.3837.
  18. Bozena Staruch and Bogdan Staruch. First order theories for partial models. Studia Logica, 80(1):105-120, 2005. Google Scholar
  19. Colin Thomas, Maximilien Cosme, Cédric Gaucherel, and Franck Pommereau. Model-checking ecological state-transition graphs. PLoS Comput. Biol., 18(6), 2022. URL: https://doi.org/10.1371/journal.pcbi.1009657.
  20. Sebastian Uchitel, Jeff Kramer, and Jeff Magee. Behaviour model elaboration using partial labelled transition systems. ACM SIGSOFT Software Engineering Notes, 28(5):19-27, 2003. Google Scholar
  21. Johan van Benthem. An essay on sabotage and obstruction. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, volume 2605 of LNCS, pages 268-276. Springer, 2005. Google Scholar
  22. Pierre Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, 28:119-136, 1985. 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