Paper Info
Title
On the analysis of safety specifications using LTL for a class of discrete event controllers applied to manufacturing systems
Abstract
A model checking procedure, based on the recently introduced linear temporal logic LTL[e] framework, is proposed for the analysis of a class of safety specifications for the synthesis of discrete-event supervisory controllers. A restricted syntax is proposed for capturing specifications which, in our experience, are common in the design of control systems for manufacturing processes. Semantic models for finite trajectories are constructed as labelled finite state machines (LFSM) based on the open-loop behaviour of the particular system under analysis. Logic consistency of the specification set is verified by model checking each LTL[e] formula against the LFSM semantic models of the rest of the specifications. The approach, although computationally intensive in the use of linear complexity algorithms, guarantees the logic correctness of the monolithic specification before executing the synthesis calculations that are of quadratic complexity. The advantages of the proposed approach are illustrated with the analysis of a specification set employed in the synthesis of a supervisor module for a manufacturing system.
Year
DOI
Venue
2011
10.1109/ICCA.2011.6138051
Control and Automation
Keywords
Field
DocType
computational complexity,discrete event systems,finite state machines,formal verification,manufacturing processes,manufacturing systems,open loop systems,safety,temporal logic,LFSM semantic model,LTL,control system design,discrete-event supervisory controller,finite trajectory,labelled finite state machine,linear complexity algorithm,linear temporal logic,logic consistency,manufacturing process,manufacturing system,model checking procedure,monolithic specification,open-loop behaviour,quadratic complexity,safety specification analysis,semantic model
Model checking,Computer science,Correctness,Linear temporal logic,Finite-state machine,Control engineering,Temporal logic,Control system,Computational complexity theory,Formal verification
Conference
ISSN
ISBN
Citations 
1948-3449
978-1-4577-1475-7
0
PageRank 
References 
Authors
0.34
6
2
Name
Order
Citations
PageRank
Arturo Sanchez1103.14
Javier Molina200.68