DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2023.23

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

Authors: Serenella Cerrito, Valentin Goranko, and Sophie Paillocher

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

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.

Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.FSCD.2023.23},
  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}
}

Document

DOI: 10.4230/LIPIcs.TIME.2019.13

Minimisation of Models Satisfying CTL Formulas

Authors: Serenella Cerrito, Amélie David, and Valentin Goranko

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{cerrito_et_al:LIPIcs.TIME.2019.13,
  author =	{Cerrito, Serenella and David, Am\'{e}lie and Goranko, Valentin},
  title =	{{Minimisation of Models Satisfying CTL Formulas}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.13},
  URN =		{urn:nbn:de:0030-drops-113718},
  doi =		{10.4230/LIPIcs.TIME.2019.13},
  annote =	{Keywords: CTL, model minimisation, bisimulation reduction, tableaux-based reduction}
}

Search Results

Documents authored by Cerrito, Serenella

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

Abstract

Cite as

Minimisation of Models Satisfying CTL Formulas

Abstract

Cite as

Thanks for your feedback!

Could not send message