Nonconflict check by using sequential automaton abstractions based on weak observation equivalence

Abstract

In Ramadge–Wonham supervisory control theory we often need to check nonconflict of plants and corresponding synthesized supervisors. For a large system such a check imposes a great computational challenge because of the complexity incurred by the composition of plants and supervisors. In this paper we present a novel procedure based on automaton abstractions, which removes internal transitions of relevant automata at each step, allowing the nonconflict check to be performed on relatively small automata, even though the original product system can be fairly large.

Introduction

Since Ramadge–Wonham supervisory control theory was proposed (Ramadge and Wonham, 1987, Wonham and Ramadge, 1987) in the 1980’s, significant improvement and extensions have been made. The Ramadge–Wonham paradigm relies on synchronous product to compose local components and specifications together, upon which a standard supervisor synthesis procedure (i.e. achieving controllability, observability and nonblockingness) is performed. Unfortunately, the computational complexity of synchronous product is exponentially high with respect to the number of components and their individual numbers of states. To overcome this complexity issue, many new synthesis approaches have been developed. For example, in Wonham and Ramadge (1988) the authors propose the concept of modularity, which is then extended to the concept of local modularity in de Queiroz and Cury (2000). When local supervisors are (locally) modular, a globally nonblocking supervisor becomes a product of local supervisors achievable through local synthesis. Recently new modular synthesis approaches have been proposed, e.g. in Feng and Wonham (2006), Hill, Tilbury, and Lafortune (2008) and Schmidt and Breindl (2008), which perform model abstractions first, upon which the standard synthesis approach is applied. In Leduc, Lawford, and Wonham (2005) the authors present a hierarchical interface-based approach, which, by imposing a specific interface invariance condition, decouples a large system into several independent local modules, and supervisor synthesis can be performed on each local module whose size is usually much smaller than the overall system.

When applying those new techniques, particularly modular approaches, we often need to check whether a collection of finite-state automata are nonconflicting with each other. Such a check is necessary for at least three reasons. First, a synthesis approach may require it, e.g. in de Queiroz and Cury (2000) and Wonham and Ramadge (1988) (local) modularity needs to be tested. Second, during synthesis if we can locate conflicting modules directly, then it is much more efficient to compute appropriate coordinators, that can resolve conflicts among local supervisors, as proposed in Feng and Wonham (2006), Hill et al. (2008) and Schmidt and Breindl (2008). Finally, even though theoretically a synthesis approach can guarantee that a supervisor is nonconflicting with a plant, practically we still need to test it because a synthesis program may contain coding errors causing incorrect results. Thus, a nonconflict check may help a user decide whether the obtained supervisor is indeed nonconflicting with the plant.

There has been some work on nonconflict testing, e.g. in, Flordal and Malik (2006)Pena, Carrilho da Cunha, Cury, and Lafortune (2008) and Pena, Cury, and Lafortune (2006) the authors propose to utilize model abstractions to avoid high complexity caused by synchronous product. The relationship between those model abstraction techniques are discussed in Malik, Flordal, and Pena (2008). To compute model abstraction (Pena et al., 2008, Pena et al., 2006) use natural projections, which are required to be observers (Wong & Wonham, 2004). The main disadvantage of using observers is that the alphabet of the codomain of a projection may need to be fairly large for the sake of achieving the observer property, potentially causing the size of the projected image too large for effective nonconflict test. To overcome this difficulty, we propose to use an automaton abstraction procedure, which is extended from the one presented in Su, van Schuppen, and Rooda (2008) and Su, van Schuppen, and Rooda (in press) by replacing the weak bisimilarity with the largest weak observation equivalence relation and revising the concept of standardized automata originally defined in Su et al. (in press) so that the nonblocking equivalence relation holds during abstraction and product, making our abstraction-based nonconflict check approach valid. Although the reduction approach in Flordal and Malik (2006) and several other approaches in the literature are based on nondeterministic automata, e.g. Flordal and Malik (2006), Flordal, Malik, Fabian, and Akesson (2007), Hill et al. (2008), Malik and Flordal (2008) and Su and Thistle (2006), they are different from ours that can be explained as follows. First, they use different equivalence relations during quotient construction, e.g. in Flordal and Malik (2006), Hill et al. (2008) and Su and Thistle (2006) the weak bisimilarity is used, and in Flordal et al. (2007) and Malik and Flordal (2008) the bisimilarity is used. As a contrast, we use the largest weak observation equivalence relation, which contains two different features compared with the (weak) bisimilarity: given two equivalent states, say $x$ and $x^{\prime }$, under the largest weak observation equivalence relation, (1) $x$ and $x^{\prime }$ must have the same marking status, which need not be true under the (weak) bisimilarity; and (2) $x$ and $x^{\prime }$ may have inequivalent ‘unobservable’ extensions (in the sense that $x$ can reach a state, say $y$, via an ‘unobservable’ string, but $x^{\prime }$ cannot reach any state $y^{\prime }$ weak observation equivalent to $y$ via an ‘unobservable’ string), which can not happen under the (weak) bisimilarity. The first feature potentially makes the state set of an abstraction larger than the one under the (weak) bisimilarity, and the second one affects the size of the state set in an opposite way. Since it is common that there are only a few marker states in a large automaton, the second feature is usually the dominant factor for state reduction, making the largest weak observation equivalence relation favored over the (weak) bisimilarity. The second feature also forces us to adopt a nonstandard way to construct the transition map of an abstraction, where two quotient states are connected only through ‘observable’ events, and no silent event is used, which is different from the standard quotient construction under the (weak) bisimilarity in those existing automaton-based abstraction techniques. Our second contribution is to present an efficient sequential abstraction procedure (SAP), which bears similarity to an algorithm called Computational Procedure for Global Consistency (CPGC) provided in Su and Wonham (2005), except that CPGC is based on natural projections, which, as we have pointed out before, is not suitable for nonconflict check unless all relevant projections are observers. The aggregative nature of SAP is also reflected in Flordal and Malik (2006). But as mentioned above, the abstraction technique of Flordal and Malik (2006) is different from ours. Our third contribution is to present a procedure for nonconflict check (PNC) using SAP, which can handle a large number of automata. The efficiency of PNC has been illustrated by experimental results.

This paper is organized as follows. In Section 2 we introduce basic concepts of languages and automata, and the problem statement of nonconflict check. Then we introduce automaton abstraction and relevant properties in Section 3. A procedure called PNC for nonconflict check based on sequential abstractions is presented in Section 4, along with experimental results. Conclusions are stated in Section 5. Long proofs are presented in the Appendix.