2018/07/18 by Liyong Lin, Lin, Liyong
Computer Science · #Distributed systems and fault tolerance #FOS: Electrical engineering #Formal Methods in Verification #Petri Nets in System Modeling #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1807.06725
openalex publication_date 2018/07/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Timed discrete-event systems (TDES), which is a modelling formalism proposed by Brandin and Wonham, can be used for modelling scheduling and production planning problems. This paper aims to show that TDES are essentially synchronous product structures. The proof is constructive in the sense that a generalized synchronous product rule is provided to generate a TDES from the activity automaton and the timer automata (that is, the syntactic description of the TDES) after some model transformation. We then also explain how the generalized synchronous product operation can be reduced into the standard synchronous product operation and how to reduce the number of (refined) events introduced in the model transformation. Thus, any software that can compute synchronous products can be used to compute a TDES from its activity automaton and its timer automata, after the model transformation.