Research On Behavioural Approximate Equivalence Of Transition System

In the area of formal method, transition system is one of the important formal models for describing software or hardware systems. Recently, in order to formally describe some practical systems, such as real-time systems, control systems, and optimization problem, a number of transition systems associated with quantitative data are introduced. In these systems, the conventional bisimulation is not very suitable to capture the equivalence relation between these systems. To overcome this problem, many notions are provided to describe approximate equivalence between systems. This thesis concerns itself with the theoretical and applied research of approximate equivalence. In theoretical area, our contributions include:(1) Approximate bisimulation and distance function are two important approaches for defining approximate equivalence between systems. In the framework of metric transition systems, Ying and Breugel adopt these two approaches to defineλ-bisimulation and behavioural pseudometric, respectively. This thesis explores the relationship between these two notions. We negate Breugel's conjecture which concerns with such relationship and establish a fixed point characterization of the distance function induced byλ-bisimulation.(2) In quantitative transition systems, this thesis introduces the notion of (η,α)-bisimilarity with the discount setting, where the first parameterηdescribes how similar two states are and the second parameterαis a discount factor. This thesis provides some properties of (η,α)-bisimilarity, explores the relationship between (η,α)-bisimilarity and Girard and Pappas'δ-approximate bisimilarity, establishes the stratification of (η,α)-bisimilarity, and studies the distance function induced by (η,α)-bisimilarity. In quantitative transition systems, de Alfaro et al. provided a notion of branching distance with discount setting. This thesis concerns itself with the relationship between branching distance and (η,α)-bisimilarity. We characterize branching distance with arbitrary discount factor in terms of (η,α)-bisimilarity. This result extends the one provided by Girard and Pappas, which characterizes branching distance withα=1 in terms ofδ-bisimilarity, to the general case. We also demonstrate that, in non-blocking and finite-branching quantitative transition systems, (η,α)-bisimilarity can be characterized based on branching distance. Theses two results reveal the intrinsic relationship between (η,α)-bisimilarity and branching distance.(3) Alternating transition systems are important formal models of open systems. In the framework of special alternating transition systems, the notion of approximate alternating bisimilarity is provided by Pola and Tabuada to capture the equivalence relation between control systems with disturbances and their finite abstraction. This thesis extends this notion to general alternating transition systems, presents some properties of this notion, provides a pattern to describe modal characterization of approximate bisimilarity, and establishes a modal characterization of approximate alternating bisimilarity in terms of alternating temporal logic. This result illustrates the intrinsic relationship between approximate behavioural equivalence and the modal properties satisfied by systems.On the other hand, we focus on the application of approximate equivalence in the formal design of linear control systems with disturbances. The formal design of control systems aims to adopt formal methods to construct the feedback controller of control systems so that the control systems satisfy the given specifications under the control. Some works have been developed for non-disturbance control system. In this area, in order to reduce the complexity and scale of control systems, finite abstractions of control systems are constructed, and then the controller of control systems can be obtained by constructing the controller of finite abstractions. This thesis aims to adopt similar method for the linear systems with disturbances. Our work contains the following:(4) This thesis presents a control strategy algorithm to find control strategies of finite abstractions of linear systems with disturbances. In non-disturbance case, finite abstractions of control systems are always conventional transition systems and some algorithms have been provided to construct control strategies of these finite abstractions. However, conventional transition systems cannot capture the different roles of controllable input and disturbance input. Thus conventional transition systems are not suitable for describing control systems with disturbances. To overcome this problem, Pola and Tabuada adopt alternating transition systems as models of linear systems with disturbances and their abstractions, but the algorithms provided for non-disturbance control systems are not suitable to find control strategies of finite abstractions of linear systems with disturbances. We present a control strategy algorithm based on the algorithm proposed by Kabanza et. al. to overcome this obstacle. Specifically, given a finite alternating transition system and a linear temporal logical formula, this algorithm can be used to indentify an initial state and a control strategy enforcing the specified temporal logical formula.(5) This thesis verifies this control strategy algorithm and demonstrates its completeness for a class of linear temporal logical formulae. Based on the total Biichi automata, a notion of total formula is introduced. We show that the control strategy algorithm is complete for total formulas. That is, given an alternating transition system and a specific total formula, if there exits an initial state and a control strategy enforcing the given specification, then the control strategy algorithm can always find such state and control strategy.(6) This thesis provides a methodology for the symbolic control of linear systems with disturbances. In non-disturbance case, two methodologies have been established based on bisimilarity and approximate bisimilarity, respectively. These two methodologies adopt similar technical route: construct finite abstractions which are (approximate) bisimilar to the original linear systems, find the controllers of finite abstractions, and then obtain the controllers of the original systems in terms of the controllers of finite abstractions. When adopting the approach based on bisimilarity, control systems and their finite abstractions are bisimilar, and then the obtained controllers enforce control systems satisfying the given specifications. However, since bisimilar systems require external behavior of two systems to be identical, it is sometimes difficult to construct the finite abstractions which are bisimilar to the original systems. Instead of such finite abstractions, Girard and Pappas proposed to construct the controllers of control systems in terms of finite abstractions which are approximately bisimilar to the original control systems. Although it is easier to construct such finite abstractions, the controller constructed by adopting Girard and Pappas'approach can only ensure that control systems approximately satisfy specifications under such control. Based on modal characterization of alternating approximate bisimilarity provided by this thesis, we present a methodology for symbolic control of linear control systems with disturbances. The key of our methodology is specification transformation. We introduce two specification transformation functions, construct the controllers of finite abstractions enforcing transformed specifications, and then make sure that the original systems satisfy the original specifications under the control. This methodology ensures that it is easy to construct the desired finite abstractions and that the controllers obtained by adopting our methodology enforce control systems strictly satisfying specifications. It should be pointed out that, in contrast to the other two methods, our methodology may decrease the possibility of the existence of the controllers of finite abstractions.