Improving HyLTL model checking of hybrid systems
The problem of model-checking hybrid systems is a long-time challenge in the scientific community. Most of the existing approaches and tools are either limited on the properties that they can verify, or restricted to simplified classes of systems. To overcome those limitations, a temporal logic call...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1307.4470v1 |
| _version_ | 1818000047755755520 |
|---|---|
| author | Davide Bresolin |
| author_facet | Davide Bresolin |
| author_sort | Davide Bresolin |
| collection | DOAJ |
| description | The problem of model-checking hybrid systems is a long-time challenge in the scientific community. Most of the existing approaches and tools are either limited on the properties that they can verify, or restricted to simplified classes of systems. To overcome those limitations, a temporal logic called HyLTL has been recently proposed. The model checking problem for this logic has been solved by translating the formula into an equivalent hybrid automaton, that can be analized using existing tools. The original construction employs a declarative procedure that generates exponentially many states upfront, and can be very inefficient when complex formulas are involved. In this paper we solve a technical issue in the construction that was not considered in previous works, and propose a new algorithm to translate HyLTL into hybrid automata, that exploits optimized techniques coming from the discrete LTL community to build smaller automata. |
| first_indexed | 2024-04-14T03:17:19Z |
| format | Article |
| id | doaj.art-bfc5abf2423c418f93c8daad80d1b04c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-14T03:17:19Z |
| publishDate | 2013-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-bfc5abf2423c418f93c8daad80d1b04c2022-12-22T02:15:26ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-07-01119Proc. GandALF 2013799210.4204/EPTCS.119.9Improving HyLTL model checking of hybrid systemsDavide BresolinThe problem of model-checking hybrid systems is a long-time challenge in the scientific community. Most of the existing approaches and tools are either limited on the properties that they can verify, or restricted to simplified classes of systems. To overcome those limitations, a temporal logic called HyLTL has been recently proposed. The model checking problem for this logic has been solved by translating the formula into an equivalent hybrid automaton, that can be analized using existing tools. The original construction employs a declarative procedure that generates exponentially many states upfront, and can be very inefficient when complex formulas are involved. In this paper we solve a technical issue in the construction that was not considered in previous works, and propose a new algorithm to translate HyLTL into hybrid automata, that exploits optimized techniques coming from the discrete LTL community to build smaller automata.http://arxiv.org/pdf/1307.4470v1 |
| spellingShingle | Davide Bresolin Improving HyLTL model checking of hybrid systems Electronic Proceedings in Theoretical Computer Science |
| title | Improving HyLTL model checking of hybrid systems |
| title_full | Improving HyLTL model checking of hybrid systems |
| title_fullStr | Improving HyLTL model checking of hybrid systems |
| title_full_unstemmed | Improving HyLTL model checking of hybrid systems |
| title_short | Improving HyLTL model checking of hybrid systems |
| title_sort | improving hyltl model checking of hybrid systems |
| url | http://arxiv.org/pdf/1307.4470v1 |
| work_keys_str_mv | AT davidebresolin improvinghyltlmodelcheckingofhybridsystems |