Temporal logic control

Abstract

Unlike the systems we discussed in previous chapters, which evolved autonomously, in this chapter we consider PWA control systems, which can be affected externally by applying a control signal. Then, it is possible to guarantee the satisfaction of a specification by trajectories of a PWA control system if an appropriate control signal is applied. We focus on fixed-parameter, PWA control systems. In Chap. 5 we discussed the problem of controlling a finite, possibly nondeterministic transition system from LTL specifications. To apply the methods presented there, in this chapter we develop an approach based on the construction of a finite abstraction for the infinite embedding of the PWA system, followed by the generation of a control strategy for the abstraction.