• DocumentCode
    3092966
  • Title

    The Ordinal-Recursive Complexity of Timed-arc Petri Nets, Data Nets, and Other Enriched Nets

  • Author

    Haddad, Serge ; Schmitz, Sylvain ; Schnoebelen, Philippe

  • Author_Institution
    Lab. Specification et Verification (LSV), ENS Cachan, Cachan, France
  • fYear
    2012
  • fDate
    25-28 June 2012
  • Firstpage
    355
  • Lastpage
    364
  • Abstract
    We show how to reliably compute fast-growing functions with timed-arc Petri nets and data nets. This construction provides ordinal-recursive lower bounds on the complexity of the main decidable properties (safety, termination, regular simulation, etc.) of these models. Since these new lower bounds match the upper bounds that one can derive from wqo theory, they precisely characterise the computational power of these so-called "enriched" nets.
  • Keywords
    Petri nets; computational complexity; decidability; formal verification; recursive functions; data nets; decidable properties; enriched nets; formal verification; ordinal-recursive complexity; ordinal-recursive lower bound; regular simulation; safety; termination; timed-arc Petri nets; Complexity theory; Encoding; Handheld computers; Petri nets; Radiation detectors; Upper bound; Vectors; Complexity theory; Petri nets; fast-growing hierarchy; formal verification; well-structured systems;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on
  • Conference_Location
    Dubrovnik
  • ISSN
    1043-6871
  • Print_ISBN
    978-1-4673-2263-8
  • Type

    conf

  • DOI
    10.1109/LICS.2012.46
  • Filename
    6280454