Title :
A Tool for Controller Synthesis via Symbolic Model Checking
Author :
Gromyko, Andrey ; Pistore, Marco ; Traverso, Paolo
Author_Institution :
DIT, Trento Univ.
Abstract :
We present a framework for the synthesis of controllers for (non-deterministic) discrete event systems with temporal logic specifications. A tool is built on top of symbolic model checking techniques and binary decision diagrams, with allows for dealing with problems of significant size. Besides, the framework allows for a (controlled) plant simulation and verification
Keywords :
binary decision diagrams; control system CAD; discrete event systems; program verification; temporal logic; binary decision diagrams; controlled plant simulation; controlled plant verification; controller synthesis; discrete event systems; symbolic model checking; temporal logic specifications; Automata; Automatic control; Boolean functions; Control system synthesis; Control systems; Data structures; Discrete event systems; Embedded system; Logic; Supervisory control;
Conference_Titel :
Discrete Event Systems, 2006 8th International Workshop on
Conference_Location :
Ann Arbor, MI
Print_ISBN :
1-4244-0053-8
DOI :
10.1109/WODES.2006.382523
