| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 427322 | Information Processing Letters | 2014 | 9 Pages |
Abstract
•Deciding if a TPTL formula describes a safety property is EXPSPACE-complete.•Deciding if a TPTL formula describes a liveness property is in 2-EXPSPACE.•We provide algorithms for these decision problems based on those for deciding safety and liveness in LTL.
We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented by Sistla [1] to decide the corresponding problems for LTL.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
David Basin, Carlos Cotrini Jiménez, Felix Klaedtke, Eugen Zălinescu,