2026-09-30T18:46:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18007 2026-09-23T18:11:03Z ddc:004 open_access

Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach Cerrito, Serenella Goranko, Valentin Paillocher, Sophie Linear temporal logic LTL partial transition systems partial model checking partial model synthesis tableaux 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Serenella Cerrito and Valentin Goranko and Sophie Paillocher 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.23 urn:nbn:de:0030-drops-180075 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.23 eng https://creativecommons.org/licenses/by/4.0/legalcode