|
PUBLIC VIVA-VOCE NOTIFICATION Wednesday, 16 June 2021, 5.30 pm Partial order reduction for timed systems Govind R Chennai Mathematical Institute. 16-06-21 Abstract In this thesis, we study the reachability problem for networks of timed automata. We focus on the issue of state-space explosion due to interleavings in these networks, and provide two different solutions for alleviating the effects of this explosion. The first is a reachability algorithm based on a local time semantics for networks of timed automata, and the second is a framework for partial order reduction methods for networks of timed automata. The standard approach for solving the reachability problem for a timed automaton involves exploring a directed graph, known as the zone graph of the timed automaton. In our work, we consider an alternate semantics for networks of timed automata, called local time semantics, which was introduced by Bengtsson et al. [CONCUR '98], and the related notion of local zone graphs. The approach in local time semantics is to make time local to each process, and synchronize the local times of processes when they execute a common action. The main challenge here is that local zone graphs are infinite in general. We overcome this challenge by designing a new algorithm that checks reachability in a network by computing a finite truncation of the local zone graph of the network. We show that multiple nodes in the standard zone graph that correspond to different interleavings of the same sequence are replaced by a single node in the local zone graph. Experimental evaluation of our algorithm shows an order of magnitude gain with respect to state of the art algorithms on several standard benchmark examples. In the second part of this thesis, we shift our focus to applying partial order reduction techniques to the exploration of local zone graphs. Partial order reduction is a widely used technique that combats the combinatorial explosion of search space by identifying a small part of the state space whose exploration is sufficient to verify the system. We describe why this is difficult to achieve in the timed setting. We then identify a subclass of networks of timed automata which we call bounded spread systems for which we develop partial order reduction algorithms. We exhibit several examples motivated by standard benchmark models that belong to this subclass. We also provide an evaluation of a prototype of the implementation of these methods using the tool TChecker.
|
