Advances in verification of time Petri nets and timed automata. A temporal logic approach.

DOI10.1007/978-3-540-32870-4MaRDI QIDQ2493434zbMATH OpenOpenAlexFDO

Authors Wojciech Penczek, Agata Półrola

Publication date 13 June 2006

Published in Studies in Computational Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-32870-4

zbMATH Keywords

temporal logictime Petri netstimed automataverification

Mathematics Subject Classification ID

Temporal logic (03B44) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

This monograph presents a comprehensive introduction to timed automata and timed Petri nets. It presents some of the existing methods of translating time Petri nets into timed automata and focuses on translations that associate clocks to various net components. Both timed and untimed temporal specification languages are introduced and model abstraction methods based on both state classes of timed Petri nets and partition refinement of timed automata are discussed. The book also presents two model checking methods, one based on exploiting abstract state spaces and the other which applies SAT-based symbolic techniques.

Recommendations

• Applications and Theory of Petri Nets 2004
• Structural translation from time Petri nets to timed automata
• From Time Petri Nets to Timed Automata: An Untimed Approach
• scientific article; zbMATH DE number 1507209
• scientific article; zbMATH DE number 2102690

Cited in

(10)

• TCTL-preserving translations from timed-arc Petri nets to networks of timed automata
• Operational semantics for timed systems. A non-standard approach to uniform modeling of timed and hybrid systems.
• Verification of Timed-Arc Petri Nets
• Specification and Verification of Multi-Agent Systems
• Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets
• scientific article; zbMATH DE number 1949608 (Why is no real title available?)
• Blending timed formal models with clock transition systems
• Applications and Theory of Petri Nets 2004
• From Time Petri Nets to Timed Automata: An Untimed Approach
• A method for parametric verification of the behavior of time Petri nets

Describes a project that uses

Uses Software

• TINA
• SPIN
• fc2tools
• Kronos
• Uppaal
• Uppaal2k
• CPN/Tools
• Design/CPN
• Chaff

This page was built for publication: Advances in verification of time Petri nets and timed automata. A temporal logic approach.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2493434)