This paper studies the path planning problem of multi-robot systems under motion uncertainties with high-level tasks that are expressed as Boolean specifications. The specification imposes logical constraints on robot trajectories and final states. First, a global Markov decision process model of the multi-robot system is constructed to provide its current state. In order to tackle the state explosion problem, at each stage, we construct a local Markov decision process for every individual agent in sequence to compute the local optimal movement strategy and update the global Markov decision process accordingly (i.e., compute locally and update globally). Next, we propose a heuristic reward function design method that provides different rewards for visiting different task points by introducing the estimated distance to complete the global task. Finally, a series of numerical experiments are conducted to demonstrate the computational efficiency and scalability of our developed approach.

In this paper a framework for engineering supervisory controllers for product lines with dynamic feature configuration is proposed. The variability in valid configurations is described by a feature model. Behavior of system components is achieved using (extended) finite automata and both behavioral and dynamic configuration constraints are expressed by means of requirements as is common in supervisory control theory. Supervisory controller synthesis is applied to compute a behavioral model in which the requirements are adhered to. For the challenges that arise in this setting, multiple solutions are discussed. The solutions are exemplified in the CIF toolset using a model of a coffee machine. A use case of the much larger Body Comfort System product line is performed to showcase feasibility for industrial-sized systems.

The paper presents a novel domain-specific language, RoboSC, for developing supervisory controllers for robotic applications. RoboSC supports concepts of ROS/ROS2 and supervisory control theory. It enables users to focus on the modeling and the synthesis process of supervisory controllers for ROS applications only because it generates all artifacts needed to connect such controllers to ROS applications and deploy them. Validation tests with actual and simulated robots show the approach's feasibility and indicate reduced coding effort.

Abstract The Eclipse Supervisory Control Engineering Toolkit (ESCET™) is an open-source project to provide a model-based approach and toolkit for developing supervisory controllers, targeting their entire engineering process. It supports synthesis-based engineering of supervisory controllers for discrete-event systems, combining model-based engineering with computer-aided design to automatically generate correct-by-construction controllers. At its heart is supervisory controller synthesis, a formal technique for the automatic derivation of supervisory controllers from the unrestricted system behavior and system requirements. Vital for the future development of these techniques and tools is the ESCET project’s open environment, allowing industry and academia to collaborate on creating an industrial-strength toolkit. We report on some crucial developments of the toolkit in the context of research projects with Rijkswaterstaat and ASML that have considerably improved its capability to deal with the complexity of real-life systems as well as its usability.

Model-based systems engineering (MBSE) enables to verify the system performance using system behavior models, which can identify design faults that do not meet the stakeholders’ requirements as early as possible, thus reducing the R&D cost and error risks. Currently, different domain engineers make use of different modeling languages to create their own behavior models. Different behavior models are verified by different approaches. It is difficult to adopt a unified integrated platform to support the modeling and verification of heterogeneous behavior models during the conceptual design phase. This paper proposes a unified modeling and verification approach supporting system formalisms and verification. The KARMA language is used to support the unified formalisms across MBSE models and dynamic simulations for different domain specific models. In order to describe the behavior model more precisely and to facilitate verification, the syntax of hybrid automata is integrated into KARMA. We implemented behavior models and their verification in MetaGraph, a multi-architecture modeling tool. Finally, the effectiveness of the proposed approach is validated by two cases: 1) the scenario of booking railway tickets using BPMN models; 2) the behavior performance simulation of unmanned vehicles using a SysML state machine diagram.

In this paper a method for engineering supervisory controllers for product lines with dynamic feature configuration is proposed. The variability in valid configurations is described by a feature model. Behavior of system components is achieved using (extended) finite automata and both behavioral and dynamic configuration constraints are expressed by means of requirements as is common in supervisory control theory. Supervisory control synthesis is applied to compute a behavioral model in which the requirements are adhered to. For the challenges that arise in this setting, multiple solutions are discussed. Some of these solutions are exemplified in the ClF tool set using a wiper system model.

Conventional supervisory control synthesis techniques are not adequate for timed automata (TA) due to their infinite state space. This paper presents a supervisory control synthesis technique for TA with the objective of satisfying controllability and nonblockingness. The synthesis method consists of three steps. First, a TA is abstracted to a finite automaton (FA). The event set of the FA includes the discrete events of the TA as well as an event representing the passage of a significant amount of time. Time passage is considered to be preemptable by events from a given set of forcible events. Second, an algorithm is presented to synthesize a controllable and nonblocking supervisor for the FA. Finally, a time-refinement technique is proposed to convert the supervisor to a TA.

A shortcoming of state-of-the-art synthesis algorithms is the lack of feedback to the user in case a supervisor cannot be synthesized or in case the supervisor is not according the expectations of the user. We present a collection of deduction rules that allow to derive reasons for the absence of a state in a supervised system and provide feedback to users. It is shown that all states for which a cause can be derived are actually omitted by synthesis and that for each omitted state a cause can be derived. An adaptation of a standard synthesis algorithm is provided that allows to automatically obtain a cause for each state that is omitted from a plant during synthesis.

The number of advanced driver assistance systems (ADASs) and the level of automation in modern vehicles is increasing at a rapid pace. Moreover, multiple of these ADASs can be active at the same time and therefore may need to interact with each other. As a consequence, the design of the supervisor layer that is responsible for proper coordination of the control tasks performed by the low-level ADASs controllers is becoming more complex and safety-critical. For this reason, there is a strong need for automated synthesis tools that lead to supervisors that are safe by design. In this paper, we present a systematic approach to model-based supervisor design using discrete-event system representations. In particular, this paper shows that the proposed method is suitable to deal with the multiple and complex systems of interacting ADASs. To be more specific, in contrast to current practice, which often relies on textual specifications and exhaustive testing, the proposed method has four main advantages: 1) it is based on mathematically specified requirements that only allow one interpretation; 2) it prevents blocking situations by design; 3) it guarantees correctness in the sense that the resulting supervisor satisfies all the specified requirements; and 4) code is generated from the obtained supervisor which eliminates the need for manual coding. The proposed method is demonstrated by means of a case study on cruise control and adaptive cruise control. The resulting supervisor is validated by simulations and experiments on a modern passenger vehicle. Based on the results presented in this paper, it can be concluded that the model-based supervisor design, simulation, and implementation method is promising and powerful for future applications in the automated vehicle systems.

This paper introduces a formal modeling approach for compositional specification of both functionality and timing of manufacturing systems. Functionality aspects can be considered orthogonally to timing aspects. The functional aspects are specified using two abstraction levels; high-level activities and lower level actions. Design of a functionally correct controller is possible by looking only at the activity level, abstracting from the different execution orders of actions and their timing. As a result, controller design can be performed on a much smaller state space compared to an explicit model where timing and actions are present. The performance of the controller can be analyzed and optimized by taking into account the timing characteristics. Since formal semantics are given in terms of a (max, +) state space, various existing performance analysis techniques can be used. We illustrate the approach, including performance analysis, on an example manufacturing system.

Domain specific languages (DSLs) ease the adoption of formal specification in industry. They allow developers to describe their specification models in concepts of their domain. However, DSLs evolve over time, causing specification models to have to co-evolve to reflect the evolution in the DSL. The maintenance overhead introduced by these, often manual, changes to specification models threatens to overshadow the advantages of DSL usage in industry. To this extent, many approaches have been proposed in the literature to facilitate DSL maintenance by automating model co-changes. In this paper, we evaluate the ability of a tool, Edapt, to support the change and co-change in twenty-two industrial DSLs and corresponding specification models over a maintenance period of four years. We observe that the tool is only able to automatically co-change specification models for 72% of the DSL changes. To address the remaining 28% of the changes, we extend Edapt. The resulting extension allows automatically co-changing specification models for 98% of the DSL changes.

Development of high-level supervisory controllers is an important challenge in the design of high-tech systems. It has become a significant issue due to increased complexity, combined with demands for verified quality, time to market, ease of development, and integration of new functionality. To deal with these challenges, model-based engineering approaches are suggested as a cost-effective way to support easy adaptation, validation, synthesis, and verification of controllers. This paper presents an industrial case study on modular design of a supervisory controller for wafer logistics in lithography machines. The uncontrolled system and control requirements are modeled independently in a modular way, using small, loosely coupled and minimally restrictive extended finite automata. The multiparty synchronization mechanism that is part of the specification formalism provides clear advantages in terms of modularity, traceability, and adaptability of the model. We show that being able to refer to variables and states of automata in guard expressions and state-based requirements, enabled by the use of extended finite automata, provides concise models. Additionally, we show how modular synthesis allows construction of local supervisors that ensure safety of parts of the system, since monolithic synthesis is not feasible for our industrial case.

This article concerns the maximal synthesis for Hennessy-Milner Logic on Kripke structures with labeled transitions. We formally define, and prove the validity of, a theoretical framework that modifies a Kripke model to the least possible extent in order to satisfy a given HML formula. Applications of this work can be found in the field of controller synthesis and supervisory control for discrete-event systems. Synthesis is realized technically by first projecting the given Kripke model onto a bisimulation-equivalent partial tree representation, thereby unfolding up to the depth of the synthesized formula. Operational rules then define the required adaptations upon this structure in order to achieve validity of the synthesized formula. Synthesis might result in multiple valid adaptations, which are all related to the original model via simulation. Each simulant of the original Kripke model, which satisfies the synthesized formula, is also related to one of the synthesis results via simulation. This indicates maximality, or maximal permissiveness, in the context of supervisory control. In addition to the formal construction of synthesis as presented in this article, we present it in algorithmic form and analyze its computational complexity. Computer-verified proofs for two important theorems in this article have been created using the Coq proof assistant.

Kripke Structures (KSs) and Labelled Transition Systems (LTSs) are the two most prominent semantic models used in concurrency theory. Both models are commonly believed to be equi-expressive. One can find many ad hoc embeddings of one of these models into the other. We build upon the seminal work of De Nicola and Vaandrager that firmly established the correspondence between stuttering equivalence in KSs and divergence-sensitive branching bisimulation in LTSs. We show that their embeddings can also be used for a range of other equivalences of interest, such as strong bisimilarity, simulation equivalence and trace equivalence. Furthermore, we extend the results by De Nicola and Vaandrager by showing that there are additional translations that allow one to use minimization techniques in one semantic domain to obtain minimal representatives in the other semantic domain for these equivalences.

Pipeless chemical plants provide an alternative way for flexible, scalable, and reconfigurable production of high valued chemical products on demand. The main feature of these pipeless plants is that the raw materials needed for production are transferred in the system by means of automated guided vehicles. Given recipes that describe the production of the desired products, the supervisory control problem is to coordinate the movement of the vehicles such that all recipes are successfully completed on time. To safely coordinate the movement of the vehicles, we propose to employ supervisory coordination. To validate timeliness and reliable completion of the recipes, we propose multiple alternatives relying on formal verification using timed and stochastic model checking.

Supervisory control theory deals with synthesis of discrete-event supervisory controllers that ensure safe (and nonblocking) behavior of the supervised system. However, the synthesized supervisor comes with no guarantees regarding desired functionality beyond nonblocking behavior. This typically occurs when the control requirements imposed on the system are too strict, or the model of the system needs to be refined. To provide concise and useful feedback to the modeler, we propose an integrated state- and event-based systems engineering framework using state-of-the-art tools: Supremica for supervisor synthesis and mCRL2 for verification. Stating properties in terms of both states and transitions is important in the domain of supervisor synthesis as many control and liveness requirements involve combined state- and event-based specifications. However, many of the available verification tools either focus on state-based or event-based properties. We seek to remedy this situation by providing verification patterns that typically occur in industrial application of supervisory control. We illustrate the framework by revisiting an industrial case study of coordinating maintenance procedures of a high-tech Oce printer, for which we verify the functionality of the solution.

The mCRL2 language is a formal specification language that is used to specify, model, analyze and verify behavioral properties for distributed systems and protocols. The semantics of the mCRL2 language is defined formally using Structural Operational Semantics (SOS). In [32] we propose an approach that takes the SOS of a formal language, along with a concrete model, that serves as an initialization, and transforms it to a Linear Process Specification (LPS). In this paper we extend the approach and show that it can be applied to a formal language that in practice is used to specify and model discussed systems. Hence, we take mCRL2's own operational semantics and transform it into an mCRL2 specification. In essence, this means that we are feeding the mCRL2 toolset its own formal language definition. This semantic dogfooding approach validates the implemented behavior for the mCRL2 language against its formal definition. By performing this exercise we revealed gaps between the defined and implemented semantics. These gaps have subsequently been resolved.

We analyze the problem of solving Boolean equation systems through the use of structure graphs . The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems with bisimilar structure graphs have the same solution. We show that our work conservatively extends earlier work, conducted by Keiren and Willemse, in which dependency graphs were used to analyze a subclass of Boolean equation systems, viz ., equation systems in standard recursive form . We illustrate our approach by a small example, demonstrating the effect of simplifying an equation system through minimization of its structure graph.

It has been our long time wish to combine the best parts of the real-time verification methods based on timed automata (TA) (the use of regions and zones), and of the process-algebraic approach of languages like LOTOS and timed muCRL. This could provide us with additional verification possibilities for real-time systems, not available in existing timed-automata-based tools like UPPAAL. In this paper we extend the applicability of such discretization to extensions of TA available in UPPAAL as networks of timed automata and shared variables. To this end, we make use of mCRL2, the newer version of muCRL that includes time and multi-actions. The multi-actions are used to model the simultaneous access to shared variables and action synchronization.

We present the first step towards combining the best parts of the real-time verification methods based on timed automata (the use of regions and zones), and of the process-algebraic approach of languages like LOTOS and muCRL. This could provide with additional verification possibilities for real-time systems, not available in existing timed-automata-based tools like UPPAAL. We aim to transfer the successful techniques of regions and zones as used for the analysis of timed automata to the realm of timed muCRL. First, we aim at replacing all parameters of sort time occurring in the resulting process equation by parameters of discrete sorts. To achieve this goal we apply process-algebraic transformations and abstraction techniques to the given process equation. As a result we obtain a process equation that is closely related to the given one in the following sense. If we abstract from the fractional parts of the time stamps in the actions, both of the equations will be timed bisimilar

In this paper, we outline a method to describe and analyze real-time systems using timed /spl mu/CRL. Most descriptions of such systems contain operators such as parallel composition that complicate analysis. As a first step towards the analysis of such systems, we linearize the given description using the algorithm from the work of Usenko (2002). The result is a timed linear process equation (TLPE) which is equivalent to the original description and has a very simple structure. Next, we outline how a TLPE can be transformed into an LPE, i.e., a linear process equation without time. This transformation, called time-free abstraction, has been used for non-recursive timed /spl mu/CRL processes in the work of Rieners et al. (2002). Crucial for this transformation is that the TLPE is transformed into a well-timed TLPE. Finally, all time-stamping is captured in the parameters of atomic actions. The result is an LPE for which the machinery of untimed /spl mu/CRL can be put to use for further analysis. These are based on symbolic analysis of the specifications, such as invariants, term rewriting and theorem proving, or on explicit state space generation and model-checking.

HyPA is an algebraic theory based on the classical process algebra Algebra of Communicating Processes (ACP) for the specification and analysis of hybrid systems. We have the idea that HyPA is also well suited for addressing various aspects of digital embedded systems including hardware, software and concurrency, as well as mixed-signal designs. To show that HyPA is useful for the specification and analysis of hybrid systems and that our idea is correct, we illustrate the use of HyPA with some case studies: a point-to-point communication , a thermostat, a positive-edge-triggered D flip flop, and a small part of a mixed-signal fuzzy controller.

While studying the specification of the operational semantics of different programming languages and formalisms, one can observe the following three facts. Firstly, Plotkin's style of structured operational semantics (SOS) has become a standard in defining operational semantics. Secondly, congruence with respect to some notion of bisimilarity is an interesting property for such languages and it is essential in reasoning about them. Thirdly, there are numerous languages that contain an explicit data part in the state of the operational semantics. The first two facts have resulted in a line of research exploring syntactic formats of operational rules to derive the desired congruence property for free. However, the third point (in combination with the first two) is not sufficiently addressed and there is no standard congruence format for operational semantics with an explicit data state. In this paper, we address this problem by studying the implications of the presence of a data state on the notion of bisimilarity. Furthermore, we propose a number of formats for congruence.

Studying industrial systems by simulation enables the designer to study the dynamic behaviour and to determine some characteristics of the system. Unfortunately simulation also has some disadvantages. These can be overcome by using formal methods. Formal methods allow a thorough analysis of the possible behaviours of a system, parameterised system analysis and a modular approach to the analysis of systems. We present a case study in which a model of an industrial system is studied in a formal way. For this purpose, the model is first specified and simulated using the CSP-based executable specification language /spl chi/. The model is translated into a model in the process algebra ACP/sup T/. This enables us to give a correctness proof of the parameterised model and to study the model in isolation.

The mechanism of Landin-style stream input/output (I/O) makes it possible to write functional programs, which behave as reactive systems when executed with lazy evaluation. Functional programming languages like Gofer are attractive for programming the data transformations of a reactive system. But although the I/O behaviour can be programmed in such languages too, the functional paradigm lacks the capabilities for specification and reasoning which are needed to analyse the communication behaviour of the program and its environment. We propose to use the Algebra of Communicating Processes (ACPet) for that purpose. The present paper attempts to bridge the gap between the functional and the process-oriented worlds. The term rewriting system of the functional language, the operational semantics of the I/O mechanism and the process equations of a program are described and their relationships are analysed. We abstract from the details of the particular programming language by using an intermediate concept of ‘abstract functional program’.

Message Sequence Charts are a widely used technique for the visualization of the communications between system components. We present a formal semantics of Basic Message Sequence Charts, exploiting techniques from process algebra. This semantics is based on the semantics of the full language as being proposed for standardization in the International Telecommunication Union.