Timed Basic Parallel Processes

15^th October 2019, 11:00
Patrick Totzke

Abstract

I will talk about two fun constructions for reachability analysis of one-clock timed automata, which lead to concise logical characterizations in existential fragment of Linear Arithmetic.

The first one describes "punctual" reachability relations: reachability in exact time t. It uses a coarse interval abstraction and counting of resets via Parikh-Automata.

The other is a "sweep line" construction to compute optimal time to reach in reachability games played on one-clock TA.

Together, these can be used to derive a (tight) NP complexity upper bound for the coverability and reachability problems in an interesting subclass of Timed Petri Nets, which naturally lends itself to parametrised safety checking of concurrent, real-time systems. This contrasts with known super-Ackermannian completeness, and undecidability results for unrestricted Timed Petri nets.

This is joint work with Lorenzo Clemente and Piotr Hofman, and was presented at CONCUR'19.
Full details are available at https://arxiv.org/abs/1907.01240

Additional Materials

• https://arxiv.org/abs/1907.01240