.png){kind=icon}
.png){kind=icon}
Return
Verifying Linear Temporal Properties on Polyhedral Systems: Decidability and Symbolic Algorithms
.png){kind=icon}
PRE
AI
DOI：10.1016/j.ic.2026.105453.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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 rp, i.e., the points from which there exists a trajectory satisfying rp.
Keywords:
Model checking
Real-time systems
LTLf
RTLf
Journal
I
IF:
1
Papers:
79
Citations:
2.8K