Evènement pour le 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.
|
Lieu | 076 |
Orateur | Shibashis Guha |
Email | shibashis@cse.iitd.ac.in |
Url | IIT Delhi |
Aucun document lié à cet événement.
RetourRetour à l'index