2026-07-26T17:25:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:21226 2024-10-22T05:39:58Z ddc:004 open_access

Model Checking Linear Temporal Properties on Polyhedral Systems Benerecetti, Massimo Faella, Marco Mogavero, Fabio Model Checking Real-Time Systems LTLf RTLf We study the problem of model checking linear temporal logic formulae on finite trajectories generated by polyhedral differential inclusions, thus enriching the landscape of models where such specifications can be effectively verified. Each model in the class comprises a static and a dynamic component. The static component features a finite set of observables represented by (non-necessarily convex) polyhedra. The dynamic one is given by a convex polyhedron constraining the dynamics of the system, by specifying the possible slopes of the trajectories in each time instant. We devise an exact algorithm that computes a symbolic representation of the region of points that existentially satisfy a given formula φ, i.e., the points from which there exists a trajectory satisfying φ. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Massimo Benerecetti and Marco Faella and Fabio Mogavero 2024 Is Part Of LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2024.19 urn:nbn:de:0030-drops-212267 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.19 eng https://creativecommons.org/licenses/by/4.0/legalcode