Search

This paper reports on recent research advances in supervisor synthesis, as well as industrial applications and future research challenges, especially in the context of a research project funded by Rijkswaterstaat, responsible for the construction and maintenance of infrastructure in the Netherlands.

The engineering of supervisory controllers for large and complex cyber-physical systems requires dedicated engineering support. The Compositional Interchange Format language and toolset have been developed for this purpose. We highlight a model-based engineering framework for the engineering of supervisory controllers and explain how the CIF language and accompanying tools can be used for typical activities in that framework such as modeling, supervisory control synthesis, simulation-based validation, verification, and visualization, real-time testing, and code generation. We mention a number of case studies for which this approach was used in the recent past. We discuss future developments on the level of language and tools as well as research results that may be integrated in the longer term.

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.

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 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 system can be fairly large.

This report defines the syntax and formal semantics of the Chi 2.0 formalism. The Chi formalism integrates concepts from dynamics and control theory with concepts from computer science, in particular from process algebra and hybrid automata. It combines a high expressivity and ease of modeling with a formal semantics. The Chi language is defined by means of an abstract and a concrete syntax. The purpose of the abstract syntax is to allow a straightforward definition of the structured operational semantics (SOS), which associates a hybrid transition system with a Chi process. The Chi Semantics is compositional, and bisimulation is a congruence for all operators. The concrete syntax offers modeling equivalents for the elements of the abstract syntax, and it introduces new syntax to ensure better readability and easier modeling. The meaning of the concrete syntax is defined by means of a mapping to the abstract syntax. The Chi language provides among others discrete, continuous, and algebraic variables, and equation process terms for modeling differential algebraic equations (DAEs), including fully implicit or switched DAEs. Steady state initialization can be specified, and higher index DAEs in Chi are equivalent to the corresponding index 1 DAEs, obtained after differentiation of the hidden constraints. The invariant process term in Chi corresponds to invariants in hybrid automata The following operators are provided (among others): the parallel composition, alternative composition (choice), and sequential composition operators; and the recursion scope operator for modeling automata. The parallel composition operator allows shared variables, shared synchronizing and non-synchronizing action labels, and shared CSP channels for synchronous communication. Two main ways of expressing urgency are provided: First, action labels and channels can be declared as urgent. Delaying is possible only if, and for as long as no urgent actions are enabled. Synchronizing actions are enabled only when the guards of all participating actions in a parallel composition are enabled. Second, urgency can be defined locally by means of the time can progress (tcp) process term, which allows delays for as long as the tcp predicate is true. Scope operators are available for hierarchical modeling. They are used to declare local variables, local action labels, and local channels. Process definition and instantiation provide process re-use and encapsulation. Hybrid automata and networks of hybrid automata can easily be expressed in Chi. Since Chi is a process algebra, its operators can be arbitrarily combined, resulting in a high modeling flexibility.

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 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 over relatively small automata, even though the original system can be fairly large.

The Chi 1.0 Language Reference Manual describes the syntax and the static semantics of all available Chi 1.0 language constructs in a compact manner. It is set up as a reference manual, intended for users that know the language but need a more precise and complete description of a construct.

Using the model-based engineering paradigm for the design of a system, the system is decomposed into several components and models are developed for these components. The models are preferably specified using domain-specific modelling formalisms. By means of co-simulation, the component models can be combined to obtain the overall system behavior. Furthermore, co-simulation enables the reuse and combination of already existing and validated subsystem models without re-entering model data. In this paper, we present a co-simulation framework that is based on the S-function interface as present in Matlab Simulink, to simulate models that consist of subsystems modelled using Matlab Simulink and subsystems modelled in the hybrid process algebra Chi. The principles of the implementation of the framework are described and the framework is illustrated by means of a bottle filling system example.