Synthesis and alternating automata over real time
<p>Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfor...
| Main Authors: | , |
|---|---|
| Outros Autores: | |
| Formato: | Thesis |
| Idioma: | English |
| Publicado em: |
2012
|
| Assuntos: |
| _version_ | 1826304819490455552 |
|---|---|
| author | Jenkins, M Mark Jenkins |
| author2 | Worrell, J |
| author_facet | Worrell, J Jenkins, M Mark Jenkins |
| author_sort | Jenkins, M |
| collection | OXFORD |
| description | <p>Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating timed automata have an undecidable language emptiness problem. In this thesis we consider restrictions on this model that restore the decidability of the language emptiness problem.</p> <p>We consider the restricted class of safety alternating timed automata, which can encode a corresponding Safety fragment of Metric Temporal Logic. This thesis connects these two formalisms with insertion channel machines, a model of faulty communication, and demonstrates that the three formalisms are interreducible. We thus prove a non-elementary lower bound for the language emptiness problem for 1-clock safety alternating timed automata and further obtain a new proof of decidability for this problem. Complementing the restriction to safety properties, we consider interpreting the automata over bounded dense time domains. We prove that the time-bounded language emptiness problem is decidable but non-elementary for unrestricted alternating timed automata.</p> <p>The language emptiness problem for alternating timed automata is a special case of a much more general and abstract logical problem: Church's synthesis problem. Given a logical specification S(I,O), Church's problem is to determine whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. It is a classical result that the synthesis problem is decidable in the case that the specification and implementation are given in monadic second-order logic over the naturals. We prove that this decidability extends to MSO over the reals with order and furthermore to MSO over every fixed bounded interval of the reals with order and the +1 relation.</p> |
| first_indexed | 2024-03-07T06:23:33Z |
| format | Thesis |
| id | oxford-uuid:f37ccc5f-8ed6-4b00-b9e3-28c4bb4ec60a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T06:23:33Z |
| publishDate | 2012 |
| record_format | dspace |
| spelling | oxford-uuid:f37ccc5f-8ed6-4b00-b9e3-28c4bb4ec60a2022-03-27T12:12:31ZSynthesis and alternating automata over real timeThesishttp://purl.org/coar/resource_type/c_db06uuid:f37ccc5f-8ed6-4b00-b9e3-28c4bb4ec60aComputer science (mathematics)Theory and automated verificationComputingMathematical logic and foundationsEnglishOxford University Research Archive - Valet2012Jenkins, MMark JenkinsWorrell, J<p>Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating timed automata have an undecidable language emptiness problem. In this thesis we consider restrictions on this model that restore the decidability of the language emptiness problem.</p> <p>We consider the restricted class of safety alternating timed automata, which can encode a corresponding Safety fragment of Metric Temporal Logic. This thesis connects these two formalisms with insertion channel machines, a model of faulty communication, and demonstrates that the three formalisms are interreducible. We thus prove a non-elementary lower bound for the language emptiness problem for 1-clock safety alternating timed automata and further obtain a new proof of decidability for this problem. Complementing the restriction to safety properties, we consider interpreting the automata over bounded dense time domains. We prove that the time-bounded language emptiness problem is decidable but non-elementary for unrestricted alternating timed automata.</p> <p>The language emptiness problem for alternating timed automata is a special case of a much more general and abstract logical problem: Church's synthesis problem. Given a logical specification S(I,O), Church's problem is to determine whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. It is a classical result that the synthesis problem is decidable in the case that the specification and implementation are given in monadic second-order logic over the naturals. We prove that this decidability extends to MSO over the reals with order and furthermore to MSO over every fixed bounded interval of the reals with order and the +1 relation.</p> |
| spellingShingle | Computer science (mathematics) Theory and automated verification Computing Mathematical logic and foundations Jenkins, M Mark Jenkins Synthesis and alternating automata over real time |
| title | Synthesis and alternating automata over real time |
| title_full | Synthesis and alternating automata over real time |
| title_fullStr | Synthesis and alternating automata over real time |
| title_full_unstemmed | Synthesis and alternating automata over real time |
| title_short | Synthesis and alternating automata over real time |
| title_sort | synthesis and alternating automata over real time |
| topic | Computer science (mathematics) Theory and automated verification Computing Mathematical logic and foundations |
| work_keys_str_mv | AT jenkinsm synthesisandalternatingautomataoverrealtime AT markjenkins synthesisandalternatingautomataoverrealtime |