Reactive Safety
The distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model checking, and synthesis problems. In this paper, we revisit the notion of safety for reactive systems, i.e., for systems w...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-06-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1106.1240v1 |
| _version_ | 1811293584635199488 |
|---|---|
| author | Rüdiger Ehlers Bernd Finkbeiner |
| author_facet | Rüdiger Ehlers Bernd Finkbeiner |
| author_sort | Rüdiger Ehlers |
| collection | DOAJ |
| description | The distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model checking, and synthesis problems. In this paper, we revisit the notion of safety for reactive systems, i.e., for systems whose behavior is characterized by the interplay of uncontrolled environment inputs and controlled system outputs. We show that reactive safety is a strictly larger class of properties than standard safety. We provide algorithms for checking if a property, given as a temporal formula or as a word or tree automaton, is a reactive safety property and for translating such properties into safety automata. Based on this construction, the standard verification and synthesis algorithms for safety properties immediately extend to the larger class of reactive safety. |
| first_indexed | 2024-04-13T05:03:37Z |
| format | Article |
| id | doaj.art-8f369b273ca44a30b6a50e71404bd755 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T05:03:37Z |
| publishDate | 2011-06-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-8f369b273ca44a30b6a50e71404bd7552022-12-22T03:01:14ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-06-0154Proc. GandALF 201117819110.4204/EPTCS.54.13Reactive SafetyRüdiger EhlersBernd FinkbeinerThe distinction between safety and liveness properties is a fundamental classification with immediate implications on the feasibility and complexity of various monitoring, model checking, and synthesis problems. In this paper, we revisit the notion of safety for reactive systems, i.e., for systems whose behavior is characterized by the interplay of uncontrolled environment inputs and controlled system outputs. We show that reactive safety is a strictly larger class of properties than standard safety. We provide algorithms for checking if a property, given as a temporal formula or as a word or tree automaton, is a reactive safety property and for translating such properties into safety automata. Based on this construction, the standard verification and synthesis algorithms for safety properties immediately extend to the larger class of reactive safety.http://arxiv.org/pdf/1106.1240v1 |
| spellingShingle | Rüdiger Ehlers Bernd Finkbeiner Reactive Safety Electronic Proceedings in Theoretical Computer Science |
| title | Reactive Safety |
| title_full | Reactive Safety |
| title_fullStr | Reactive Safety |
| title_full_unstemmed | Reactive Safety |
| title_short | Reactive Safety |
| title_sort | reactive safety |
| url | http://arxiv.org/pdf/1106.1240v1 |
| work_keys_str_mv | AT rudigerehlers reactivesafety AT berndfinkbeiner reactivesafety |