Control problems in a temporal logic framework

1 October 1986

journal article
research article
Published by Taylor & Francis in International Journal of Control

Vol. 44 (4) , 943-976
https://doi.org/10.1080/00207178608933645

Abstract

Linear-time temporal logic is applied to the verification of control systems. A formal language and proof system are adapted from those used in the verification of concurrent programs by Manna and Pnueli. Properties of some simple control systems are then verified by formally deducing temporal logic specifications of desired behaviour from descriptions of system dynamics. Finally, the usefulness of temporal logic in control theory is discussed and topics for future research are suggested.

Keywords

This publication has 9 references indexed in Scilit:

Supervisory control of a class of discrete event processes
Published by Springer Nature ,2005
Hardware Verification
Computer, 1985
Synthesis of Communicating Processes from Temporal Logic Specifications
ACM Transactions on Programming Languages and Systems, 1984
Specifying Concurrent Program Modules
ACM Transactions on Programming Languages and Systems, 1983
Modular Verification of Computer Communication Protocols
IEEE Transactions on Communications, 1983
Using branching time temporal logic to synthesize synchronization skeletons
Science of Computer Programming, 1982
Verifying Concurrent Processes Using Temporal Logic
Published by Springer Nature ,1982
The Science of Programming
Published by Springer Nature ,1981
Self-stabilizing systems in spite of distributed control
Communications of the ACM, 1974