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

Volume

2

fYear

1996

fDate

11-13 Dec 1996

Firstpage

2243

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Decision and Control, 1996., Proceedings of the 35th IEEE Conference on

Conference_Location

Kobe

ISSN

0191-2216

Print_ISBN

0-7803-3590-2

Type

conf

DOI

10.1109/CDC.1996.572984

Filename

572984