Semantic tableau for control of PLTL formulae
Akash Deshpande, Pravin P. Varaiya · 2002
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.