Options
Abstractions for the local-time semantics of timed automata: A foundation for partial-order methods
Journal
Proceedings - Symposium on Logic in Computer Science
ISSN
10436871
Date Issued
2022-08-02
Author(s)
Govind, R.
Herbreteau, Frédéric
Srivathsan, B.
Walukiewicz, Igor
Abstract
A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods when solving the reachability problem for timed networks. It is based on a local-time semantics proposed by [Bengtsson et al. 1998]. A new simulation based abstraction of local-time zones is proposed. The main technical contribution is an efcient algorithm for testing subsumption between local-time zones with respect to this abstraction operator. The abstraction is not fnite for all networks. It turns out that, under relatively mild conditions, there is no fnite abstraction for local-time zones that works for arbitrary timed networks. To circumvent this problem, we introduce a notion of a bounded-spread network. The spread of a network is a parameter that says how far the local times of individual processes need to diverge. For boundedspread networks, we show that it is possible to use subsumption and partial-order methods at the same time.
Subjects