Evènement pour le groupe
Modélisation et Verification
Date  20130307 11:3012:30 
Titre  A semidecidable approach for determining language inclusion for timed automata 
Résumé  Language inclusion for timed automata is known to be undecidable. The
universality problem can be considered to be a special case of the
language inclusion problem. Given a universal timed automaton A and any
other timed automaton B, the language inclusion problem asks if the timed
language accepted by A is included in the timed language accepted by B.
Solving this problem implies deciding the universality problem for B which
is known to be undecidable!
In this work, we present a semidecidable algorithm which gives three
outputs as follows: 'yes' indicates that we conclude that the language
accepted by A is a subset of the language accepted by B. 'no' indicates
that the language accepted by timed automaton B does not include the
language accepted by A. 'do not know' indicates that we do not know how
the langauges accepted by A and B are related.
The language inclusion problem for timed automata is known to be decidable
when timed automaton B is deterministic or determinizable or when timed
automaton B (strongly time) simulates timed automaton A or when B is a
single clock timed automaton. We show that our method works in many cases
where B cannot simulate A or B cannot be determinized.

Lieu  076 
Orateur  Shibashis Guha 
Email  shibashis@cse.iitd.ac.in 
Url  IIT Delhi 
Aucun document lié à cet événement.
RetourRetour à l'index