Cyber-physical systems (CPSs) are systems with both physical and software components, for example, cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this article, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into signal temporal logic. The second addition is the use of valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification.

In order to develop a computationally efficient implementation of the maximally permissive deadlock avoidance policy (DAP) for complex resource allocation systems (RAS), a recent approach focuses on the identification of a set of critical states of the underlying RAS state-space, referred to as minimal boundary unsafe states. The availability of this information enables an expedient one-step-lookahead scheme that prevents the RAS from reaching outside its safe region. The work presented in this paper seeks to develop a symbolic approach, based on binary decision diagrams (BDDs), for efficiently retrieving the (minimal) boundary unsafe states from the underlying RAS state-space. The presented results clearly demonstrate that symbolic computation enables the deployment of the maximally permissive DAP for complex RAS with very large structure and state-spaces with limited time and memory requirements. Furthermore, the involved computational costs are substantially reduced through the pertinent exploitation of the special structure that exists in the considered problem. Note to Practitioners-A key component of the real-time control of many flexibly automated operations is the management of the allocation of a finite set of reusable resources among a set of concurrently executing processes so that this allocation remains deadlock-free. The corresponding problem is known as deadlock avoidance, and its resolution in a way that retains the sought operational flexibilities has been a challenging problem due to: (i) the inability to easily foresee the longer-term implications of an imminent allocation and (ii) the very large sizes of the relevant state spaces that prevent an online assessment of these implications through exhaustive enumeration. A recent methodology has sought to address these complications through the offline identification and storage of a set of critical states in the underlying state space that renders efficient the safety assessment of any given resource allocation. The results presented in this paper further extend and strengthen this methodology by complementing it with techniques borrowed from the area of symbolic computation; these techniques enable a more compressed representation of the underlying state spaces and of the various subsets and operations that are involved in the pursued computation.

A generic state-vector transition (SVT) model is suggested, including a flexible synchronous composition involving both shared variables and events. This model is analyzed, focusing on properties that are important for supervisor synthesis. A synthesis procedure is then developed for the SVT model, where supervisor guards are generated that guarantee a controllable, nonblocking and maximally permissive supervisor. Novel conditions are introduced, such that more flexible specifications can be applied than earlier suggested for related models. Since the SVT model includes automata and (colored) Petri nets, optionally extended with variables, guards and actions, as special cases, the suggested synthesis approach unifies supervisor synthesis for the main discrete event model classes. Finally, the SVT model is naturally represented and efficiently computed based on binary decision diagrams, and the resulting supervisor guards are easily implemented in industrial control systems.

In this paper, we symbolically represent timed discrete-event systems (TDES), which can be used to efficiently compute the supervisor in the supervisory control theory context. We model a TDES based on timed extended finite automata (TEFAs): an augmentation of extended finite automata (EFAs) by incorporating discrete time into the model. EFAs are ordinary automata extended with discrete variables, where conditional expressions and update functions can be attached to the transitions. The symbolic computations are based on binary decision diagrams (BDDs). We show how TEFAs can be represented by BDDs. The main feature of this approach is that the BDD-based fixed point computations are not based on tick models that have been commonly used in this area, leading to better performance in many cases. The approach has been implemented and applied to a simple case study and several large-scale benchmarks.

In supervisory control theory, a supervisor restricts the plant in order to fulfill given specifications. A problem for larger industrial applications is that the resulting supervisor is not easily implemented and comprehensible for the users. To tackle this problem, an efficient method has recently been introduced to characterize a supervisor by tractable logic conditions, referred to as guards. This approach has been developed for a specific type of automata with variables called extended finite automata (EFAs). An extension of this approach to a more general class of models is presented in this paper. It means that classical supervisory control problems for automata and Petri nets are easily and efficiently solved, but also generalized based on the suggested approach. The synthesis procedure is naturally modeled and efficiently computed based on binary decision diagrams.

The sequential behavior of a manufacturing system results from several constraints introduced during the product, manufacturing, and control logic development. This paper proposes methods and algorithms for automatically representing and visualizing this behavior from various perspectives throughout the development process. A new sequence planning approach is introduced that uses self-contained operations to model the activities and execution constraints. These operations can be represented and visualized from multiple perspectives using a graphical and formal language called Sequences of Operations (SOPs). The operations in a manufacturing system are related to each other in various ways, due to execution constraints expressed by operation pre- and post-conditions. These operation relations include parallel, sequence, arbitrary order, alternative, and hierarchy relations. Based on the SOP language, these relations are identified and visualized in various SOPs and sequences. A software tool, Sequence Planner, has been developed, for organizing the operations into SOPs that visualize only relevant operations and relations.

In flexible manufacturing systems a large number of operations need to be coordinated and supervised to avoid blocking and deadlock situations. The synthesis of such supervisors soon becomes unmanageable for industrial manufacturing systems, due to state space explosion. In this paper we therefore develop some reduction principles for a recently presented model based on self-contained operations and sequences of operations. First sequential operation behaviors are identified and related operation models are simplified into one model. Then local transitions without interaction with other operation models are removed. This reduction principle is applied to a synthesis of non-blocking operation sequences, where collisions among moving devices are guaranteed to be avoided by a flexible booking process. The number of states in the synthesis procedure and the computation time is reduced dramatically by the suggested reduction principle.

In the supervisory control theory, a supervisor is generated based on given plant and specification models. The supervisor restricts the plant in order to fulfill the specifications. A problem that is typically encountered in industrial applications is that the resulting supervisor is not easily comprehensible for the users. To tackle this problem, we introduce an efficient method to characterize a supervisor by tractable logic conditions, referred to as guards, generated from the models. The guards express under which conditions an event is allowed to occur to fulfill the specifications. To obtain tractable guard expressions, we reduce them by exploiting the structure of the given models. In order to be able to handle complex systems efficiently, the models are symbolically represented by binary decision diagrams and all computations are performed on these data structures. The algorithms have been implemented in a supervisory control tool and applied to an industrially relevant example.