Practical Controller Synthesis for MTL$0,∞$

3 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Metric Temporal Logic MTL$0,∞$ is a timed extension of linear temporal logic, LTL, with time intervals whose left endpoints are zero or whose right endpoints are infinity. Whereas the satisfiability and model-checking problems for MTL$0,∞$ are both decidable, we note that the controller synthesis problem for MTL$0,∞$ is unfortunately undecidable. As a remedy of this we propose an approximate method to the synthesis problem, which we demonstrate to be adequate and scalable to practical examples. We define a method for converting MTL$0,∞$ formulas into (nondeterministic) Timed Game Büchi Automata and furthermore show how to construct determinized over-and underapproximation of a such. For the proposed method, we present a toolchain seamlessly integrating the needed components for practical MTL$0,∞$ synthesis. Lastly we demonstrate on a number of case-studies the applicability and scalability of the proposed method.
Type de document :
Communication dans un congrès
International SPIN Symposium on Model Checking of Software, Jul 2017, Santa barbara United States. 〈10.1145/nnnnnnn.nnnnnnn〉
Domaine :

Littérature citée [24 références]

https://hal.inria.fr/hal-01642162
Contributeur : Nisrine Jafri <>
Soumis le : mardi 21 novembre 2017 - 00:54:33
Dernière modification le : jeudi 11 janvier 2018 - 06:28:15

Fichier

spin.pdf
Fichiers produits par l'(les) auteur(s)

Citation

Guangyuan Li, Peter Jensen, Kim Larsen, Axel Legay, Danny Poulsen. Practical Controller Synthesis for MTL$0,∞$. International SPIN Symposium on Model Checking of Software, Jul 2017, Santa barbara United States. 〈10.1145/nnnnnnn.nnnnnnn〉. 〈hal-01642162〉

Métriques

Consultations de la notice

275

Téléchargements de fichiers