Bibliografía

Liveness of Safe Object Nets

Michael Köhler-Bußmeier and Frank Heitmann.
Liveness of safe object nets.
In Louchka Popova-Zeugmann, H.-D. Burkhard, Ludwik Czaja, W. Penczek, G. Lindemann, A. Skowron, and Z. Suraj, editors, Proceedings of the International Workshop on Concurrency, Specification, and Programming, CS&P'2010, Helenenau, September 27-29 (Volume 1), volume 237 of Informatik-Bericht, pages 198-209. Humboldt-Universität zu Berlin, sep 2010.  [link]

Resumen: In this paper we study the complexity of the liveness problem for safe Elementary Object Nets (Eos). Object nets are Petri nets which have Petri nets as tokens. They are called elementary if the net system has a two levelled structure. The concept of safeness bounds the number of tokens which may reside on a place. We will use four different safeness definitions (first introduced in [10]) and show that the liveness problem is undecidable for safe(1) and safe(2) Eos and in Pspace for safe(3) and safe(4) Eos. We will devise an polynomial space algorithm for this problem and indeed for every property that can be expressed in the temporal logic CTL.

BibTeX registro

@InProceedings{Koehler+10d,
  author =   {K{\"o}hler-Bu{\ss}meier, Michael and Heitmann, Frank},
  title =   {Liveness of Safe Object Nets},
  editor = {Popova-Zeugmann, Louchka and Burkhard, H.-D. and Czaja, Ludwik
            and Penczek, W. and Lindemann, G. and Skowron, A. and Suraj, Z.},
  booktitle =  {Proceedings of the International Workshop
                on Concurrency, Specification, and Programming, CS{\&}P'2010,
                Helenenau, September 27-29 (Volume 1)},
  publisher = {Humboldt-Universit\"{a}t zu Berlin},
  year =  {2010},
  month = {sep},
  pages  = {198--209},
  volume = {237},
  series = {Informatik-Bericht},
  abstract = {In this paper we study the complexity of the liveness
problem for safe Elementary Object Nets (Eos).
Object nets are Petri nets which have Petri nets as tokens. They are
called elementary if the net system has a two levelled structure. The
concept of safeness bounds the number of tokens which may reside on a
place.
We will use four different safeness definitions (first introduced in [10])
and show that the liveness problem is undecidable for safe(1) and safe(2)
Eos and in Pspace for safe(3) and safe(4) Eos.
We will devise an polynomial space algorithm for this problem and indeed
for every property that can be expressed in the temporal logic CTL.},
  url = {http://www2.informatik.hu-berlin.de/ki/CSP2010/proc.html}
}

Copyright Notice

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.