Revised Version of "Dynamic Real-Time CEGAR for Timed Automata Created and Destroyed at Run Time"

Model checking of timed automata suffers from state explosion caused by dense time and parallel composition. In systems whose configuration changes during operation, such as dynamically reconfigurable processors, composing all modules statically makes this worse. This paper proposes Dynamic Real-Time CEGAR, a counterexample-guided abstraction refinement loop for networks of dynamic timed automata, in which automata are created and destroyed at run time and the set of clocks therefore changes along an execution. Reachability is checked on a finite predicate abstraction of clock valuations. Abstract counterexamples are checked by an exact backward zone analysis that uses the new zone operations Add and Del, and spurious counterexamples are eliminated by adding predicates. We prove soundness and termination: every set computed by the backward analysis is a union of clock regions, which guarantees that refinement makes progress. We further show that the bound on the number of refinements depends only on the clocks of running automata, whereas the bound guaranteed under static composition grows with the square of the total number of clocks. Experiments on four benchmark families show that the numbers of predicates and abstract states stay constant when the timing constants grow by three orders of magnitude, whereas exact zone exploration grows proportionally. Neither the LU extrapolation of UPPAAL, the aLU simulation of TChecker, nor the lazy abstraction of Theta removes this growth. It arises when independently reset clocks run periodically under equality guards; in Fischer's protocol and train-gate with constants enlarged by three orders of magnitude, the number of states of exact zone exploration does not change either. We also show that dynamic composition reduces the dimension of difference bound matrices to the number of running modules, but active-clock reduction on the static model reaches the same state space and, if freed clocks are removed from the matrices, the same or a smaller dimension. However, on models with many reachable configurations the refinement loop is the bottleneck, and the proposed method is slower than exact zone exploration.