Identifying state coding conflicts in asynchronous system specifications using Petri net unfoldings
Document typeConference report
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Rights accessOpen Access
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder
State coding conflict detection is a fundamental part of synthesis of asynchronous concurrent systems from their specifications as signal transition graphs (STGs), which are a special kind of labelled Petri nets. The paper develops a method for identifying state coding conflicts in STGs that is intended to work within a new synthesis framework based on Petri net unfolding. The latter offers potential advantages due to a partial order representation of highly concurrent behaviour as opposed to the more traditional construction of a state graph, known to suffer from combinatorial explosion. We develop a necessary condition for coding conflicts to exist, by using an approximate state covering approach. Being computationally easy, yet conservative, such a solution may produce fake conflicts. A technique for refining the latter with extra computational cost, is provided.
CitationKondratyev, A. [et al.]. Identifying state coding conflicts in asynchronous system specifications using Petri net unfoldings. A: International Conference on Application of Concurrency to System Design. "1998 International Conference on Application of Concurrency to System Design: March 23-26, 1998, Fukushima, Japan: proceedings". Institute of Electrical and Electronics Engineers (IEEE), 1998, p. 152-163.