Compositional Analysis for Safety Specifications

This project extends compositional statistical model checking for autonomous vehicles from Markovian to non-Markovian safety specifications.

The core idea is to augment simulation states with DFA states that encode the temporal logic of the specification, then propagate the DFA distribution across primitive scenario traces. This makes it possible to verify safety properties that depend on the history of events (not just the current state) while preserving the compositional structure that keeps large-scale verification tractable.