|A semi-decidable approach for determining language inclusion for timed automata|
du groupe Modélisation et Verification
|Date|| 2013-03-07 11:30-12:30|
|Titre||A semi-decidable 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 semi-decidable 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.
|Orateur||Shibashis Guha |
|Url||IIT Delhi |
Aucun document lié à cet événement.RetourRetour à l'index