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 φ.
@InProceedings{benerecetti_et_al:LIPIcs.TIME.2024.19, author = {Benerecetti, Massimo and Faella, Marco and Mogavero, Fabio}, title = {{Model Checking Linear Temporal Properties on Polyhedral Systems}}, booktitle = {31st International Symposium on Temporal Representation and Reasoning (TIME 2024)}, pages = {19:1--19:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-349-2}, ISSN = {1868-8969}, year = {2024}, volume = {318}, editor = {Sala, Pietro and Sioutis, Michael and Wang, Fusheng}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.19}, URN = {urn:nbn:de:0030-drops-212267}, doi = {10.4230/LIPIcs.TIME.2024.19}, annote = {Keywords: Model Checking, Real-Time Systems, LTLf, RTLf} }
Feedback for Dagstuhl Publishing