Template-Based Controller Synthesis for Timed Systems

Autor:	Bernd Finkbeiner, Hans-Jörg Peter
Rok vydání:	2012
Předmět:	Set (abstract data type) Template Control theory Computer science Observability Granularity Algorithm Parametric statistics Undecidable problem Automaton
Zdroj:	Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642287558 TACAS
DOI:	10.1007/978-3-642-28756-5_27
Popis:	We present an effective controller synthesis method for real-time systems modeled as timed automata with safety requirements. Under the realistic assumption of partial observability, the problem is undecidable in general, and prohibitively expensive (2ExpTime-complete) if a bound on the granularity of the controller is set in advance. We investigate the synthesis of controllers from templates, given as timed automata with parametric control structure. Template-based synthesis is significantly cheaper (PSpace-complete) than standard synthesis and produces much simpler controllers. We present an efficient symbolic synthesis algorithm based on automatic abstraction refinement and report on encouraging experimental results from an implementation in the timed verification and synthesis tool synthia.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::0359d1f21b6b0cd85a31a6dbdebf47a0 https://doi.org/10.1007/978-3-642-28756-5_27 Zobrazit plný text záznamu