R | |
---|---|

[RSM19] | Victor Roussanaly,
Ocan Sankur, and
Nicolas Markey.
Abstraction Refinement Algorithms for Timed
Automata.
In CAV'19,
Lecture Notes in Computer Science 11561, pages 22-40. Springer-Verlag, July 2019.
- Abstract
We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.
@inproceedings{cav2019-RSM, author = {Roussanaly, Victor and Sankur, Ocan and Markey, Nicolas}, title = {Abstraction Refinement Algorithms for Timed Automata}, editor = {Dillig, I{\c s}il and Ta{\c s}iran, Serdar}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'19)}, acronym = {{CAV}'19}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {11561}, pages = {22-40}, year = {2019}, month = jul, doi = {10.1007/978-3-030-25540-4_2}, abstract = {We~present abstraction-refinement algorithms for model checking safety properties of timed automata. The~abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We~implement this idea in two~ways: an~enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.}, } |

- 1
- 1
- 1