CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Supervisory Control using Satisfiability Solvers

Alexey Voronov (Institutionen för signaler och system, Automation) ; Knut Åkesson (Institutionen för signaler och system, Automation)
Discrete Event Systems, 2008. WODES 2008. 9th International Workshop on p. 81-86. (2008)
[Konferensbidrag, refereegranskat]

This paper discusses how satisfiability solvers may be used to verify and synthesize discrete event supervisors as defined in the supervisory control theory. By using the supervisory control theory it is possible to generate control functions that are correct by construction. However, the computations for verification and synthesis of the supervisors are NP-complete and in order to make the method applicable for industrial use it is necessary to use algorithms and tools that could solve problems of industrial size. Within the model checking community satisfiability solvers have become an important tool for verification of large hardware circuits. In this paper it is shown how to formulate some problems in the supervisory control theory as Boolean satisfiability problems. Formulations of satisfiability problems for synthesizing a path to a marked state, verification of controllability and verification of deadlock presence are presented. The method is evaluated on some examples of high complexity.

Nyckelord: supervisory control, satisfiability solvers, model checking, discrete event system

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2009-01-15. Senast ändrad 2012-01-13.
CPL Pubid: 87498


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)


Teoretisk datalogi

Chalmers infrastruktur