License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.23
URN: urn:nbn:de:0030-drops-180075
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18007/
Go to the corresponding LIPIcs Volume Portal

Cerrito, Serenella ; Goranko, Valentin ; Paillocher, Sophie

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

pdf-format:
LIPIcs-FSCD-2023-23.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{cerrito_et_al:LIPIcs.FSCD.2023.23,
  author =	{Cerrito, Serenella and Goranko, Valentin and Paillocher, Sophie},
  title =	{{Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18007},
  URN =		{urn:nbn:de:0030-drops-180075},
  doi =		{10.4230/LIPIcs.FSCD.2023.23},
  annote =	{Keywords: Linear temporal logic LTL, partial transition systems, partial model checking, partial model synthesis, tableaux}
}

Keywords: Linear temporal logic LTL, partial transition systems, partial model checking, partial model synthesis, tableaux
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI