The notion of observable liveness was introduced in the literature for 1-safe Petri net systems in which transitions are either observable or unobservable by a user and, among the observable ones, some are controllable, in the sense that they correspond to interactions with the user and cannot autonomously occur. An observable transition is observably live if a user can, from any reachable marking, force it to occur infinitely often by using controllable transitions. Here, we introduce a weaker version of this notion by considering the capability of the user, by means of controllable transitions, to force the considered observable transition to fire infinitely often, starting from the initial marking instead of considering each reachable marking. The main result of this paper is a method for checking weak observable liveness in state machine decomposable 1- safe nets whose transitions are observable. The introduced method is based on infinite games that are played on finite graphs. We transform the problem of weak observable liveness into a game between a system and a user, and we prove that a transition is weakly observably live if and only if the user has a winning strategy for the game.

Bernardinello, L., Kılınç, G., Pomello, L. (2017). Weak observable liveness and infinite games on finite graphs. In Application and Theory of Petri Nets and Concurrency 38th International Conference, PETRI NETS 2017 (pp.181-199). Springer Verlag [10.1007/978-3-319-57861-3_12].

Weak observable liveness and infinite games on finite graphs

Bernardinello, L
;
Kılınç, G;Pomello, L
2017

Abstract

The notion of observable liveness was introduced in the literature for 1-safe Petri net systems in which transitions are either observable or unobservable by a user and, among the observable ones, some are controllable, in the sense that they correspond to interactions with the user and cannot autonomously occur. An observable transition is observably live if a user can, from any reachable marking, force it to occur infinitely often by using controllable transitions. Here, we introduce a weaker version of this notion by considering the capability of the user, by means of controllable transitions, to force the considered observable transition to fire infinitely often, starting from the initial marking instead of considering each reachable marking. The main result of this paper is a method for checking weak observable liveness in state machine decomposable 1- safe nets whose transitions are observable. The introduced method is based on infinite games that are played on finite graphs. We transform the problem of weak observable liveness into a game between a system and a user, and we prove that a transition is weakly observably live if and only if the user has a winning strategy for the game.
No
paper
Petri nets; Infinite games; Observable liveness; Theoretical Computer Science; Computer Science (all)
English
International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017
9783319578606
2017
Bernardinello, L., Kılınç, G., Pomello, L. (2017). Weak observable liveness and infinite games on finite graphs. In Application and Theory of Petri Nets and Concurrency 38th International Conference, PETRI NETS 2017 (pp.181-199). Springer Verlag [10.1007/978-3-319-57861-3_12].
Bernardinello, L; Kılınç, G; Pomello, L
File in questo prodotto:
File Dimensione Formato  
Bernardinello2017_Chapter_WeakObservableLivenessAndInfin.pdf

Solo gestori archivio

Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Dimensione 618.27 kB
Formato Adobe PDF
618.27 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/187660
Citazioni
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 0
Social impact