Nicolas Markey

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.},
}