Paper Info
Title
A Supervisory Control Algorithm Based on Property-Directed Reachability.
Abstract
We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The discrete event systems framework is useful in both software, automation and manufacturing, as problems from those domains can be modelled as discrete supervisory control problems. As a formal framework, DES is also similar to domains for which the field of formal methods for computer science has developed techniques and tools. In this paper, we attempt to marry the two by adapting PDR to the problem of controller synthesis. The resulting algorithm takes as input a transition system with forbidden states and uncontrollable transitions, and synthesises a safe and minimally-restrictive controller, correct-by-design. We also present an implementation along with experimental results, showing that the algorithm has potential as a part of the solution to the greater effort of formal supervisory controller synthesis and verification.
Year
DOI
Venue
2017
10.1007/978-3-319-70389-3_8
Haifa Verification Conference
DocType
Volume
ISSN
Journal
abs/1711.06501
Strichman O., Tzoref-Brill R. (eds) Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science, vol 10629. Springer, Cham
Citations 
PageRank 
References 
0
0.34
9
Authors
4
Name
Order
Citations
PageRank
Koen Claessen1146896.88
Jonatan Kilhamn200.34
Laura Kovács349436.97
Bengt Lennartson4934118.87