Horn Clauses for Communicating Timed Systems
Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1412.1153v1 |
| _version_ | 1819264605672701952 |
|---|---|
| author | Hossein Hojjat Philipp Rümmer Pavle Subotic Wang Yi |
| author_facet | Hossein Hojjat Philipp Rümmer Pavle Subotic Wang Yi |
| author_sort | Hossein Hojjat |
| collection | DOAJ |
| description | Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular Uppaal timed automata), exhibit limited scalability for systems with large discrete state space, or cannot handle parametrised systems. We explore the use of Horn constraints and off-the-shelf model checkers for analysis of networks of timed automata. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, and can be extended to include various language features, for instance Uppaal-style communication/broadcast channels and BIP-style interactions, and systems with infinite parallelism. Experiments demonstrate the feasibility of the method. |
| first_indexed | 2024-12-23T20:32:09Z |
| format | Article |
| id | doaj.art-5c263f70a11f45a28d97c1a545361574 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-23T20:32:09Z |
| publishDate | 2014-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-5c263f70a11f45a28d97c1a5453615742022-12-21T17:32:11ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-12-01169Proc. HCVS 2014395210.4204/EPTCS.169.6:4Horn Clauses for Communicating Timed SystemsHossein Hojjat0Philipp Rümmer1Pavle Subotic2Wang Yi3 Cornell University, USA Uppsala University, Sweden Uppsala University, Sweden Uppsala University, Sweden Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular Uppaal timed automata), exhibit limited scalability for systems with large discrete state space, or cannot handle parametrised systems. We explore the use of Horn constraints and off-the-shelf model checkers for analysis of networks of timed automata. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, and can be extended to include various language features, for instance Uppaal-style communication/broadcast channels and BIP-style interactions, and systems with infinite parallelism. Experiments demonstrate the feasibility of the method.http://arxiv.org/pdf/1412.1153v1 |
| spellingShingle | Hossein Hojjat Philipp Rümmer Pavle Subotic Wang Yi Horn Clauses for Communicating Timed Systems Electronic Proceedings in Theoretical Computer Science |
| title | Horn Clauses for Communicating Timed Systems |
| title_full | Horn Clauses for Communicating Timed Systems |
| title_fullStr | Horn Clauses for Communicating Timed Systems |
| title_full_unstemmed | Horn Clauses for Communicating Timed Systems |
| title_short | Horn Clauses for Communicating Timed Systems |
| title_sort | horn clauses for communicating timed systems |
| url | http://arxiv.org/pdf/1412.1153v1 |
| work_keys_str_mv | AT hosseinhojjat hornclausesforcommunicatingtimedsystems AT philipprummer hornclausesforcommunicatingtimedsystems AT pavlesubotic hornclausesforcommunicatingtimedsystems AT wangyi hornclausesforcommunicatingtimedsystems |