Invited Session 9
Synthesis of Discrete Event Systems for Correct-byConstruction Cyber Physical Systems
Submission code: sjua3
School of Electrical and Electronic Engineering, Nanyang Technological University, 50 Nanyang Avenue, Singapore 639798
Tel: +65 8587-1091 Email: firstname.lastname@example.org
Cyber physical systems are the integrations of computation, networking and physical processes, which are ubiquitous in our modern society. The modelling formalism of discrete-event systems has been used to model cyber physical systems, based on the primitive notion of events and event-based transitions. The synthesis of discrete-event systems provides a framework for correct-by-construction cyber physical systems, which is able to address the issues of safety, progress and resilience. This invited session aims to report recent research achievements, including new tools and techniques that are developed to support the verification and synthesis of discrete event systems for correct-by-construction cyber physical systems, and identify some potential research
directions and challenges.
I THE GOAL OF THIS INVITED SESSION AND ITS COHESIVE STRUCTURE
The goal of this session is to report recent research achievements related to the synthesis of discrete-event systems, to identify relevant research directions and challenges.
This includes timed synthesis and untimed synthesis, networked synthesis and non-networked synthesis, as well as the synthesis of DES models. In this session, Paper 1 investigates the non-blocking supervisory control of timed automaton, which is inherently of infinite state space due to the modelling of dense time and leads to well known undecidability result. Conventional finite state automaton based synthesis technique cannot be directly applied. Thus, Paper 1 proposes an abstraction-based approach to perform non-blocking timed supervisor synthesis for timed automata. Paper 2 then considers the untimed, non-networked synthesis, where a topological approach is adopted to synthesize the supremal sublanguages arising from the supervisory control theory and some open questions are discussed for this approach. Paper 3 addresses the networked supervisor synthesis problem over bounded channels with bounded delays, by using a generalized modelling formalism to model the message transmission process. Page 4 considers the synthesis (i.e., the learning) of DES models with logging and behaviour reconstruction. As a result, simulation and analysis, and even supervisor synthesis, can be performed on the learnt DES models. A movable bridge is used as a case study to show the applicability of the method