Title :
Semantic tableau for control of PLTL formulae
Author :
Deshpande, Akash ; Varaiya, Pravin
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA
Abstract :
We describe the propositional linear temporal logic (PLTL) formalism and introduce the notions of observations, actions and control in PLTL. We develop the 0-lag and 0-lead possibly blocking and nonblocking control strategies and describe their properties. We present an algorithm to generate finite semantic tableaux for control of PLTL formulae. The semantic tableau is part of the controller state and at each time it classifies the actions available to the controller into three groups: those that would immediately complete the task, those that would postpone task completion and those that would immediately block task completion for ever. The tableau reflects the syntactic structure of the PLTL formula under consideration. The algorithm yields the tableau for the 0-lag possibly blocking control strategy
Keywords :
closed loop systems; controllability; discrete event systems; observability; temporal logic; 0-lag possibly blocking control; 0-lag possibly nonblocking control; 0-lead possibly blocking control; 0-lead possibly nonblocking control; actions; finite semantic tableaux; observations; propositional linear temporal logic; syntactic structure; task completion; Automata; Automatic control; Closed loop systems; Control system synthesis; Control systems; Discrete event systems; Logic; Open loop systems;
Conference_Titel :
Decision and Control, 1996., Proceedings of the 35th IEEE Conference on
Conference_Location :
Kobe
Print_ISBN :
0-7803-3590-2
DOI :
10.1109/CDC.1996.572984
