• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

On Temporal Properties of Nested Petri Nets

P. 122-127.
Dworzanski L. W., Frumin D. I.

Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.