1 Search Results for "Paillocher, Sophie"

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}
}
  • Refine by Author
  • 1 Cerrito, Serenella
  • 1 Goranko, Valentin
  • 1 Paillocher, Sophie

  • Refine by Classification

  • Refine by Keyword
  • 1 Linear temporal logic LTL
  • 1 partial model checking
  • 1 partial model synthesis
  • 1 partial transition systems
  • 1 tableaux

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

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 About DROPS Imprint Privacy Contact