Search

The analysis of industrial processes, modelled as descriptor systems, is often computationally hard due to the presence of both algebraic couplings and difference equations of high order. In this paper, we introduce a control refinement notion for these descriptor systems that enables analysis and control design over related reduced-order systems. Utilising the behavioural framework, we extend upon the standard hierarchical control refinement for ordinary systems and allow for algebraic couplings inherent to descriptor systems., Comment: 8 pages, 3 figures

Supervisor:緒方 和博, 先端科学技術研究科, 修士（情報科学）

We present a formal characterization of fault-tolerant behaviors of computing systems via simulation relations. This formalization makes use of variations of standard simulation relations in order to compare the executions of a system that exhibits faults with executions where no faults occur; intuitively, the latter can be understood as a specification of the system and the former as a fault-tolerant implementation. By employing variations of standard simulation algorithms, our characterization enables us to algorithmically check fault-tolerance in polynomial time, i.e., to verify that a system behaves in an acceptable way even subject to the occurrence of faults. Furthermore, the use of simulation relations in this setting allows us to distinguish between the different levels of fault-tolerance exhibited by systems during their execution. We prove that each kind of simulation relation preserves a corresponding class of temporal properties expressed in CTL; more precisely, masking fault-tolerance preserves liveness and safety properties, nonmasking fault-tolerance preserves liveness properties, while failsafe fault-tolerance guarantees the preservation of safety properties. We illustrate the suitability of this formal framework through its application to standard examples of fault-tolerance. Fil: Demasi, Ramiro Adrian. Fondazione Bruno Kessler; Italia Fil: Castro, Pablo Francisco. Universidad Nacional de Rio Cuarto. Facultad de Cs.exactas Fisicoquímicas y Naturales. Departamento de Computación. Grupo de Ingeniería de Software; Argentina Fil: Maibaum, Thomas S. E.. Mcmaster University. Faculty Of Engineering; Canadá Fil: Aguirre, Nazareno Matias. Mcmaster University. Faculty Of Engineering; Canadá. Universidad Nacional de Rio Cuarto. Facultad de Cs.exactas Fisicoquímicas y Naturales. Departamento de Computación. Grupo de Ingeniería de Software; Argentina

Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain $$10^9$$ vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games.

Compositional analysis techniques such as assume-guarantee reasoning are frequently used in computer science to validate the design of complex process models. Since many engineering systems are built modularly from interconnections of components, the resulting mathematical models can be arbitrarily complex, which makes their analysis equally challenging. This paper presents a framework of how to apply compositional and assume-guarantee reasoning to linear time-invariant (LTI) systems. A key tool are simulation relations which are used to relate systems models with their specifications as well as to determine abstractions of given system behaviors. First, complex systems defined by standard feedback interconnections are considered. Parallel composition of LTI systems, the second type of interconnections, introduces algebraic constraints but allows for decomposition of a global specification.

Quotienting by simulation equivalences is a well-established technique for reducing the size of nondeterministic Büchi automata. We adapt this technique to alternating Büchi automata. To this end we suggest two new quotients, namely minimax and semi-elective quotients, prove that they preserve the recognized languages, and show that computing them is not more difficult than computing quotients for nondeterministic Büchi automata. Our approach is game-theoretic; the proofs rely on a specifically tailored join operation for strategies in simulation games which is interesting in its own right. We explain the merits of our quotienting procedures with respect to converting alternating Büchi automata into nondeterministic ones.

The complexity of physical and engineering systems, both in terms of the governing physical phenomena and the number of subprocesses involved, is mirrored in ever more complex mathematical models. While the demand for precise models is indisputable, the analysis of such system models remains challenging. Adopting techniques from computer science makes available a framework for compositional analysis of interconnected control systems. Simulation relations relate process models with their specifications thus checking whether the derived model behaves as desired. Based on that, compositional and assume-guarantee reasoning rules decompose the actual verification task into several subtasks that can be checked with less computational effort. Thus, modularly composed system models can be treated with modular analysis techniques. In this paper, we want to give an overview of how these concepts can be applied to analyze linear continuous-time systems (LTI). Motivated by the underlying physics, we introduce a general type of interconnection that can also be interpreted as a feedback control configuration in the spirit of decentralized control. Additionally, parallel composition of LTI systems is discussed with special emphasis on decomposition strategies for a given specification. The proposed methodology could be extended further to classes of hybrid systems where compositional analysis techniques are of particular interest.

The complexity of physical and engineering systems, both in terms of the governing physical phenomena and the number of subprocesses involved, is mirrored in ever more complex mathematical models. While the demand for precise models is indisputable, the analysis of such system models remains challenging. Adopting techniques from computer science makes available a framework for compositional analysis of interconnected control systems. Simulation relations relate process models with their specifications thus checking whether the derived model behaves as desired. Based on that, compositional and assume-guarantee reasoning rules decompose the actual verification task into several subtasks that can be checked with less computational effort. Thus, modularly composed system models can be treated with modular analysis techniques. In this paper, we want to give an overview of how these concepts can be applied to analyze linear continuous-time systems (LTI). Motivated by the underlying physics, we introduce a general type of interconnection that can also be interpreted as a feedback control configuration in the spirit of decentralized control. Additionally, parallel composition of LTI systems is discussed with special emphasis on decomposition strategies for a given specification. The proposed methodology could be extended further to classes of hybrid systems where compositional analysis techniques are of particular interest.

The complexity of physical and engineering systems, both in terms of the governing physical phenomena and the number of subprocesses involved, is mirrored in ever more complex mathematical models. While the demand for precise models is indisputable, the analysis of such system models remains challenging. Adopting techniques from computer science makes available a framework for compositional analysis of interconnected control systems. Simulation relations relate process models with their specifications thus checking whether the derived model behaves as desired. Based on that, compositional and assume-guarantee reasoning rules decompose the actual verification task into several subtasks that can be checked with less computational effort. Thus, modularly composed system models can be treated with modular analysis techniques. In this paper, we want to give an overview of how these concepts can be applied to analyze linear continuous-time systems (LTI). Motivated by the underlying physics, we introduce a general type of interconnection that can also be interpreted as a feedback control configuration in the spirit of decentralized control. Additionally, parallel composition of LTI systems is discussed with special emphasis on decomposition strategies for a given specification. The proposed methodology could be extended further to classes of hybrid systems where compositional analysis techniques are of particular interest.

We analyze simulation relations as heuristics for the simplification of omega-automata, i.e., of finite automata working on infinite strings. Our focus is on alternating omega-automata. We introduce direct, delayed, and fair simulation for alternating Büchi automata (ABA) and show that these relations are preorders, they imply language containment, and they can be computed in polynomial time. We introduce quotient constructions for ABA suited for direct and delayed simulation, and we show that our notions of simulation are compatible with the standard translation of ABA to non-alternating automata. We apply these results to the problem of translating formulas of propositional linear-time temporal logic (LTL) to nondeterministic automata. We develop a translation algorithm from LTL to equivalent nondeterministic automata with an on-the-fly use of simulation relations for simplification, and we compare our approach to tableau-based translation algorithms. We extend our notion of delayed simulation to alternating parity automata (APA), introduce variants of this relation suited for quotienting of APA, and develop a simulation-based simplification algorithm for APA. We give a sketch of how to apply these results to a fragment of the modal mu-calculus.