TY - GEN
T1 - Negotiation programs
AU - Esparza, Javier
AU - Desel, Jörg
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - We introduce a global specification language for distributed negotiations, a recently introduced concurrent computation model with atomic negotiations combining synchronization of participants and choice as primitive. A token game on distributed negotiations determines reachable markings which enable possible next atomic negotiations. In a deterministic distributed negotiation, each participant can always be engaged in at most one next atomic negotiation. In a sound distributed negotiation, every atomic negotiation is enabled at some reachable marking, and from every reachable marking the final marking of the distributed negotiation can be reached. We prove that our specification language has the same expressive power as sound and deterministic negotiations, i.e., every program can be implemented by an equivalent sound and deterministic negotiation and every sound and deterministic negotiation can be specified by an equivalent program, where a program and a negotiation are equivalent if they have the same Mazurkiewicz traces and thus the same concurrent runs. The translations between negotiations and programs require only linear time.
AB - We introduce a global specification language for distributed negotiations, a recently introduced concurrent computation model with atomic negotiations combining synchronization of participants and choice as primitive. A token game on distributed negotiations determines reachable markings which enable possible next atomic negotiations. In a deterministic distributed negotiation, each participant can always be engaged in at most one next atomic negotiation. In a sound distributed negotiation, every atomic negotiation is enabled at some reachable marking, and from every reachable marking the final marking of the distributed negotiation can be reached. We prove that our specification language has the same expressive power as sound and deterministic negotiations, i.e., every program can be implemented by an equivalent sound and deterministic negotiation and every sound and deterministic negotiation can be specified by an equivalent program, where a program and a negotiation are equivalent if they have the same Mazurkiewicz traces and thus the same concurrent runs. The translations between negotiations and programs require only linear time.
UR - http://www.scopus.com/inward/record.url?scp=84937428667&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-19488-2_8
DO - 10.1007/978-3-319-19488-2_8
M3 - Conference contribution
AN - SCOPUS:84937428667
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 157
EP - 178
BT - Application and Theory of Petri Nets and Concurrency - 36th International Conference, PETRI NETS 2015, Proceedings
A2 - Devillers, Raymond
A2 - Valmari, Antti
PB - Springer Verlag
T2 - 36th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2015
Y2 - 21 June 2015 through 26 June 2015
ER -