Determinization of timed Petri nets behaviors
| Autor: | Jean-Louis Boimond, Sébastien Lahaye, Jan Komenda |
|---|---|
| Přispěvatelé: | Laboratoire Angevin de Recherche en Ingénierie des Systèmes (LARIS), Université d'Angers (UA) |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Discrete mathematics
0209 industrial biotechnology Formal power series Computer science Concurrency Liveness 02 engineering and technology Petri net (max + ) automata Semiring Nondeterministic algorithm [SPI]Engineering Sciences [physics] 020901 industrial engineering & automation Control and Systems Engineering Modeling and Simulation Bounded function 0202 electrical engineering electronic engineering information engineering Stochastic Petri net 020201 artificial intelligence & image processing Electrical and Electronic Engineering determinization Computer Science::Formal Languages and Automata Theory timed Petri nets |
| Zdroj: | Discrete Event Dynamic Systems Discrete Event Dynamic Systems, 2015, pp.1-25. ⟨10.1007/s10626-015-0214-1⟩ |
| ISSN: | 1573-7594 |
| DOI: | 10.1007/s10626-015-0214-1⟩ |
| Popis: | In this paper we are interested in sequentialization of formal power series with coefficients in the semiring (źź{źź},max,+)$(\mathbb {R}\cup \{- \infty \},\max ,+)$ which represent the behavior of timed Petri nets. Several approaches make it possible to derive nondeterministic (max, + ) automata modeling safe timed Petri nets. Their nondeterminism is a serious drawback since determinism is a crucial property for numerous results on (max, + ) automata (in particular, for applications to performance evaluation and control) and existing procedures for determinization succeed only for restrictive classes of (max, + ) automata. We present a natural semi-algorithm for determinization of behaviors based on the semantics of bounded timed Petri nets. The resulting deterministic (max, + ) automata can be infinite, but a sufficient condition called strong liveness is proposed to ensure the termination of the semi-algorithm. It is shown that strong liveness is closely related to bounded fairness, which has been widely studied for Petri nets and other models for concurrency. Moreover, if the net cannot be sequentialized we propose a restriction of its logical behavior so that the sufficient condition becomes satisfied for the restricted net. The restriction is based on the synchronous product with non injectively labeled scheduler nets that are built in an incremental hierarchical way from simple scheduler nets. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink