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

Supervisory Control of Discrete-Event Systems via IC3

Mohammad Reza Shoaei (Institutionen för signaler och system, Automation) ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Bengt Lennartson (Institutionen för signaler och system, Automation)
10th International Haifa Verification Conference, HVC 2014 Vol. 8855 (2014), p. 252-266.
[Konferensbidrag, refereegranskat]

The IC3 algorithm has proven to be an effective SAT-based safety model checker. It has been generalized to other frameworks such as SMT and applied very successfully to hardware and software model checking. In this paper, we present a novel technique for the supervisory control of discrete-event systems with infinite state space via IC3. We introduce an algorithm for synthesizing maximally permissive controllers using a generalized IC3 to find (if any exists) a weakest inductive invariant predicate which holds in the initial state, is maintained as the system evolves, and implies safety and control properties. To this end, we use a variation of IC3, called Tree-IC3, as a bug finder to solve the supervisory predicate control problem by iteratively reporting all feasible counterexample traces using a tree-like search, while controlling the system to avoid them. The maximally permissiveness is achieved by finding the weakest of such controllers that is invariant under safety and control properties. Experimental results demonstrate the great potential of using IC3 technique for the purpose of the supervisory control problems.

Nyckelord: Discrete-event systems, Supervisory control theory, Incremental inductive verification, IC3



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-09-11. Senast ändrad 2016-08-22.
CPL Pubid: 202658

 

Läs direkt!


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