Efficient Verification of Timed Automata
Advisors :
F. Herbreteau,
and I. Walukiewicz
Keywords
Real-time Systems, Model-checking, Timed Automata, Algorithmics.
Description
Timed automata[1] are finite automata extended with clocks that can be
reset and tested on the transitions. Clocks hence measure the delay
between actions of the automaton. Timed automata are widely used to
model real-time systems and for model-checking real-time
specifications.
Clocks are real-valued variables, hence the state-space of a timed
automaton is infinite (and even not countable). To overcome this
problem, verification algorithms use a symbolic representation of the
executions of the automaton. The symbolic representation must further
be abstracted[2] in order to guarantee its finiteness. The efficiency
of the verification algorithms heavily rely on the coarseness of the
abstraction[3].
These last years, we have proposed several optimizations of the
abstractions and the underlying algorithms[4,5,6,7,8,9]. The goals of
this thesis are:
- to develop new abstractions that could dynamically use
the informations that are collected by verification algorithms,
- to study which are the properties preserved by these abstractions
(in particular, regarding probabilistic and quantitative/priced
extensions of timed automata),
- the combination to verification techniques for distributed
systems.
Bibliography
- [1] R. Alur and D. Dill. A Theory of Timed
Automata. Theoretical Computer Science, 126: 183-235,
1994.
- [2] C. Daws and S. Tripakis. Model checking
of real-time reachability properties using
abstractions. Int. Conf. on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS), LNCS vol. 1384,
Springer, 1998.
- [3] G. Behrmann and P. Bouyer and
K.G. Larsen and R. Pelanek. Lower and upper bounds in
zone-based abstractions of timed automata. Int. J. on Software
Tools for Technology Transfer (STTT), 8(3): 204-215, 2006.
- [4] F. Herbreteau, B. Srivathsan and
I. Walukiewicz. Efficient Emptiness Check for Timed Büchi
Automata. Proc 22nd Int. Conf. on Computer Aided Verification
(CAV), 2010.
- [5] F. Herbreteau and
B. Srivathsan. Efficient On-The-Fly Emptiness Check for
Timed Büchi Automata. Proc. 8th Int. Symp. on Automated
Technology for Verification and Analysis (ATVA), 2010.
- [6] F. Herbreteau and B. Srivathsan. Coarse
abstractions make Zeno behaviors difficult to detect. Proc. 22nd
Int. Conf. on Concurrency Theory (CONCUR), 2011.
- [7] F. Herbreteau, D. Kini,
B. Srivathsan and I. Walukiewicz. Using non-convex
approximations for efficient analysis of timed
automata. Proc. 31st Int. Conf. on Foundations of Software
Technology and Theoretical Computer Science (FSTTCS), 2011.
- [8] F. Herbreteau, B. Srivathsan and
I. Walukiewicz. Efficient Emptiness Check for Timed Büchi
Automata. Formal Methods in System Design, Special Issue
Selected Papers CAV10 Conference, Accepted for publication.
- [9] F. Herbreteau, B. Srivathsan and
I. Walukiewicz. Better abstractions for timed automata. CoRR/1110.3705. Submitted