Name
Abstract | ||
|---|---|---|
Verification of temporal logic properties plays a crucial role in proving the desired behaviors of hybrid systems. In this paper, we propose an interval method for verifying the properties described by a bounded linear temporal logic. We relax the problem to allow outputting an inconclusive result when verification process cannot succeed with a prescribed precision, and present an efficient and rigorous monitoring algorithm that demonstrates that the problem is decidable. This algorithm performs a forward simulation of a hybrid automaton, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. A continuous state at a certain time computed in each step is enclosed by an interval vector that is proven to contain a unique solution. In the experiments, we show that the proposed method provides a useful tool for formal analysis of nonlinear and complex hybrid systems. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1016/j.entcs.2015.10.009 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
Hybrid systems,interval analysis,linear temporal logic,bounded model checking | Discrete mathematics,Interval temporal logic,Algorithm,Linear temporal logic,Decidability,Temporal logic,Interval arithmetic,Hybrid system,Mathematics,Hybrid automaton,Bounded function | Journal |
Volume | Issue | ISSN |
abs/1506.01762 | C | 1571-0661 |
Citations | PageRank | References |
1 | 0.36 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daisuke Ishii | 1 | 5 | 1.50 |
| Naoki Yonezaki | 2 | 107 | 20.02 |
| Alexandre Goldsztejn | 3 | 161 | 21.42 |