Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Incremental Language Inclusion Checking for Networks of Timed Automata
verfasst von : Willibald Krenn, Dejan Ničković, Loredana Tec
Erschienen in: Formal Modeling and Analysis of Timed Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Checking the language inclusion between two models is a fundamental problem arising in application areas such as formal verification or refinement in top-down design. We propose an incremental procedure for checking the language inclusion between two real-time specifications, modeled as networks of deterministic timed automata, where the two specifications are equivalent up to one component. For such classes of systems we aim to improve the efficiency of the language inclusion check by exploiting the compositional nature of the problem and avoiding the explicit parallel composition of the timed automata in the network. We first develop a generic procedure that gives freedom to specific implementation choices. We then propose an instantiation of the procedure that is based on bounded model checking techniques. We illustrate the application of our approach in a case study and discuss promising experimental results.