Compositional Verification of Finite Automata under Event Preemption

Given a number of synchronised automata, com-positional verification seeks to verify non-conflictingness with-out the explicit computation of an overall model. Technically, the approach alternates conflict-preserving abstractions with the composition of a small number of strategically chosen automata and the literature reports substantial computational benefits for examples of practical relevance. In this paper, we re-visit this approach in order to address the situation of preemptive events, i.e., events that are known beforehand to be scheduled at highest priority. Our study is motivated by high-level programming languages commonly used in industrial automation, where events associated with actuators preempt events associated with sensors.