Quotient-based Approach to Control of Discrete-Event Systems with Mu-Calculus Specification

Quicklinks to: Members, Description, Publications, Tool Version 1, NEW Tool Version 2, Example.

Project Members

 Samik Basu, Department of Computer Science, Iowa State University.
Ratnesh Kumar, Department of Electrical and Computer Engineering, Iowa State University.

Project Description

 We study the control of a discrete-event system (DES) subject to a control specification expressed in propositional mu-calculus under complete observation of events. Solution is obtained through "quotienting": Given a plant automaton model and a mu-calculus specification we provide a set of quotienting rules that can be used to compute the ``quotient'' of the specification formula with respect to the plant. The quotient is another mu-calculus formula with the property that a supervisor exists if and only if the quotiented formula is satisfiable. Thus the control problem is reduced to one of mu-calculus satisfiability. We also present a tableau-based satisfiability solving algorithm that generates a model for quotiented formula.

Our solution takes into consideration (a) nondeterminism in the plant model, (b) state-based uncontrollability and unobservability constraints. Uncontrollability constraint defines events that cannot be disabled by the controller while unobservability constraint defines events that are unobservable and event-classes that are indistinguishable.

Publications

  1. Samik Basu and Ratnesh Kumar
    Quotient-based Control Synthesis for Non-Deterministic Plants with Mu-Calculus Specifications .IEEE Conference on Decision and Control 2006
    Download powerpoint poster
    Tool: Handles nondeterminism and state-based uncontrollability constraints in the plant models. Download the tool

  2. Samik Basu and Ratnesh Kumar
    Quotient-based Control Synthesis for Partially Observed Nondeterministic Plants. Submitted 2007
    Tool: Handles nondeterminism and state-based uncontrollability and unobservability constraints in the plant models. Download the tool

Illustrative Example

 Consider the maze of 5 rooms shown in the Figure 1 where a cat and a mouse move. The rooms are labeled 0 through 4 and are interconnected via a number of doorways. Each doorway is assigned a direction and has an exclusive accessibility either for the mouse or the cat: doorway accessible by the mouse is denoted by mi while that accessible by the cat is denoted ci. All doorways with the exception of c7 are controllable. Initially the cat and the mouse are in the rooms 2 and 4 respectively.
Figure 1.
The behavior of the cat and the mouse can be represented using finite state machines where each state represents the room and a transition represents the movement from one room to another via a doorway (transition label). The transition structure of the cat and mouse behavior is illustrated in Figure 2. The product of the cat and the mouse state machines generates the plant model Figure 3.
Figure 2.
Figure 3.
An objective is to find a supervisor which does not allow the cat and the mouse to occupy the same room simultaneously. This specification can be written as a mu-calculus formula
νX.(p /\ [-]X)
where p represents a proposition which is true only when the cat and the mouse are not in the same room. We use a short-hand notation [-] to represent any action. The greatest fixed point formula represents the states where p holds and this continues to remain true after any action. The supervisor for the plant model is shown in Figure 4. Each state in the supervisor model is annotated with the partitions where the cat and the mouse are present.
Figure 4.
A more general objective is that in the controlled system the cat and the mouse do not occupy the same room simultaneously, and also it is possible for the cat and the mouse to be able return to the start state from any state. This more general specification can be written as
νY.(μZ.(q\/ <->Z)/\ p /\ [-]Y)
where p has the usual meaning and q represents a proposition which is true only when the cat and the mouse are at their respective start states (i.e. the cat is in room 2 and the mouse is in room 4). The greatest fixed point formula over the variable Y has a nested least fixed point formula over the variable Z. The least fixed point formula represents the states which can eventually reach the start state while the outer greatest fixed point formula ensures that the cat and the mouse are never in the same room. The supervisor for the plant model satisfying the general objective is shown in Figure 5. In the plant model, we considered nondeterminism by renaming c4 to c1.
Figure 5.
Finally, we consider two pairs of observably indistinguishable actions c1 vs c4 and c3 vs m6 in addition to uncontrollable action c7. The corresponding controller for the specification νX.(p /\ [-]X) is shown in Figure 6. Observe that the controller behaves identically following the indistinguishable actions.
Figure 6.