Evènement pour le groupe Modélisation et Verification


Date 2013-03-07  11:30-12:30
TitreA 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.  
Lieu076 
OrateurShibashis Guha 
Emailshibashis@cse.iitd.ac.in 
UrlIIT Delhi 



Aucun document lié à cet événement.

Retour
Retour à l'index