Abstractions pour les automates temporisés

SRIVATHSAN, Balaguru

Metadata

Show full item record

License

SRIVATHSAN, Balaguru

Language

Thèses de doctorat

Date

2012

Speciality

Informatique

Doctoral school

École doctorale de mathématiques et informatique (Talence, Gironde)

Abstract

Cette thèse revisite les problèmes d'accessibilité et de vivacité pour les au-tomates temporisés.L'accessibilité est couramment résolue par le calcul d'un arbre de recherche abstrait. L'abstraction est paramétrée par des bornes provenant des gardes de l'automate. Nous montrons que l'abstraction a 4LU de Behrmann et al. est la plus grande abstraction saine et complète pour les bornes LU. N' étant pas convexe, elle n'est pas mise en oeuvre dans les outils. Nous introduisons une méthode qui permet son utilisation éfficace. Finalement, nous proposons une optimisation des bornes à la volée exploitant le calcul de l'arbre.Le problème de vivacité requiert de détecter les exécutions Zenon/non-Zenon. Une solution standard ajoute une horloge à l'automate. Nous montrons qu'elle conduit a une explosion combinatoire. Nous proposons une solution qui évite ce problème pour une grande classe d'abstractions. Pour les abstractions LU nous montrons que détecter ces exécutions est un problèmeNP-complet.Read less <

English Abstract

We consider the classic model of timed automata introduced by Alurand Dill. Two fundamental properties one would like to check in this modelare reachability and liveness. This thesis revisits these classical problems.The reachability problem for timed automata asks if there exists a run ofthe automaton from the initial state to a given final state. The standard solutionto this problem constructs a search tree whose nodes are abstractionsof zones. For effectiveness, abstractions are parameterized by maximal lowerand upper bounds (LU-bounds) occurring in the guards of the automaton.Such abstractions are also termed as LU-abstractions. The a4LU abstractiondefined by Behrmann et al is the coarsest known LU-abstraction. Althoughit is potentially most productive to use the a4LU abstraction, it has not beenused in implementations as it could lead to non-convex sets. We show howone could use the a4LU abstraction efficiently in implementations. Moreover,we prove that a4LU abstraction is optimal: given only the LU-bound information,it is the coarsest possible abstraction that is sound and completefor reachability. We then concentrate on ways to get better LU-bounds. Inthe standard procedure the LU-bounds are obtained from a static analysisof the automaton. We propose a new method to obtain better LU-boundson-the-fly during exploration of the zone graph. The potential gains of proposedimprovements are validated by experimental results on some standardverification case studies.The liveness problem deals with infinite executions of timed automata.An infinite execution is said to be Zeno if it spans only a finite amountof time. Such runs are considered unrealistic. While considering infiniteexecutions, one has to eliminate Zeno runs or dually, find runs that arenon-Zeno. The B¨uchi non-emptiness problem for timed automata asks ifthere exists a non-Zeno run visiting an accepting state infinitely often. Thestandard solution to this problem adds an extra clock to take care of non-Zenoness. We show that this solution might lead to an exponential blowupin the search space. We propose a method avoiding this blowup for a wideclass of abstractions weaker than LU-abstractions. We show that such amethod does not exist for LU-abstractions unless P=NP. Another questionrelated to infinite executions of timed automata is to decide the existenceof Zeno runs. We provide the first complete solution to this problem. Itworks for a wide class of abstractions weaker than LU. Yet again, we showthe solution could lead to a blowup for LU-abstractions, unless P=NP.Read less <

Keywords

Automate temporisés

Abstractions

Algorithmes à la volée

Exécution Zenon

English Keywords

Ti:ed automata

Finite abstractions

On-the-fly algorithms

Zenoness

URI

https://oskar-bordeaux.fr/handle/20.500.12278/21066

Origin

STAR imported

Metadata

Share this item!

License