The SCAN Statistical Model Checker

Enrico Ghiorzi; Armando Tacchella

cs.FLMar 24, 2026

The SCAN Statistical Model Checker

Authors: Enrico Ghiorzi, Armando Tacchella

Organizations: Università di Genova

Abstract

This paper lays out the formal foundations upon which the SCAN statistical model checker is built.

Figures & tables

\fontspec_if_language:nTF ENG \addfontfeature Language=EnglishFigure 1: A taxonomy of models.

Model	Definition	Dynamic (informal)	Dynamic (formal)
TS	$(S,\Act,\longrightarrow,I,\AP,L)$	Transition Relation	$\longrightarrow\subseteq S\times\Act\times S$
PTS	$(S,\Act,p,I,\AP,L)$	Transition Probability	$p:S\times\Act\times S\to[0,1]$
TTS	$(S,\Act,\longrightarrow,I,X,\AP,L)$	Timed Trans. Relation	$\longrightarrow\subseteq S\times\Act\times 2^{X}\times\Phi(X)\times S$
PTTS	$(S,\Act,p,I,X,\AP,L)$	Timed Trans. Probability	$p:S\times\Act\times 2^{X}\times\Phi(X)\times S\to[0,1]$
$S$ : set of states — $\Act$ : set of actions — $I\subseteq S$ : initial states
$AP$ atomic propositions — $L:S\to 2^{\AP}$ labeling function

\fontspec_if_language:nTF ENG \addfontfeature Language=EnglishTable 1: Synopsis of transitions systems.

Model	Definition	Dynamic
PG	$(\Loc,\Act,\Effect,\hookrightarrow,\Loc_{0},g_{0})$	$\Effect:\Eval(\Var)\times\Act\to\Eval(\Var)$
		$\hookrightarrow\;\subseteq\;\Loc\times\Act\times\Cond(\Var)\times\Loc$
PPG	$(\Loc,\Act,\Effect_{p},\hookrightarrow,\Loc_{0},g_{0})$	$\Effect_{p}:\Eval(\Var)\times\Act\times\Eval(\Var)\to[0,1]$
		$\hookrightarrow\;\subseteq\;\Loc\times\Act\times\Cond(\Var)\times\Loc$
TPG	$(\Loc,\Act,\Effect,\hookrightarrow,\Loc_{0},g_{0})$	$\Eval_{t}:\Clocks\to\mathbb{Q}^{+}$
		$\Effect:\Eval(\Var)\times\Eval_{t}(\Clocks)\times\Act\to\Eval(\Var)\times\Eval_{t}(\Clocks)$

\fontspec_if_language:nTF ENG \addfontfeature Language=EnglishTable 2: Synopsis of program graphs.

	executable if…	effect
$!(p,q,x)$	$(p,q)$ is not full	$Enqueue((p,q),x)$
$!(p,q,{<}m{>})$	$(p,q)$ is not full	$Enqueue((p,q),m)$
$?(q,p,x)$	$(p,q)$ is not empty	$\langle x\coloneqq Front((p,q));Dequeue((p,q))\rangle$
$?(q,p,{<}m{>})$	$(p,q)$ is not empty and the sent value is equal to $m$	$Dequeue((p,q))$

\fontspec_if_language:nTF ENG \addfontfeature Language=EnglishTable 3: Enabledness and effect of communication actions if

cap((p,q))>0

Panel of Figure 5 — \fontspec_if_language:nTF ENG \addfontfeature Language=EnglishFigure 3: Simplified class diagram for SCAN.

Explore similar work

Scenario-Based Compositional Statistical Model Checking for Safety Specifications
Oct 4, 2026Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang +2Formal Verification
University of California, Berkeley, USA
Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes
Jun 24, 2026Konstantin Kueffner, Tobias Meggendorfer, Maximilian Weininger +1Markov Decision Processes Uncertainty Quantification
Institute of Science and Technology Austria, Klosterneuburg, Austria · Lancaster University Leipzig, Leipzig, Germany · Ruhr-University Bochum, Bochum, Germany +1
Beyond F1: Evaluating Coverage and Failure Recovery in AI Model Security Scanners
Aug 27, 2026Qianlong Lan, Vinothini Pandurangan, Anuj Kaul +1Static Code Analysis
eBay Inc.

Oct 4, 2026J/K move · Enter open · S save

Scenario-Based Compositional Statistical Model Checking for Safety Specifications

Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang, Beyazit Yalcinkaya+1

University of California, Berkeley, USA

Formal Verification

Open paper AskPDF arXiv

In safety-critical domains such as autonomous driving, systems must be evaluated across a large number of environment conditions, often represented as composite scenarios built from primitive scenarios. Existing statistical model checking (SMC) approaches analyze each composite scenario independently, requiring many expensive simulations and resulting in substantial redundant computation when scenarios share common structure. This work introduces a scenario-based compositional SMC framework for safety and co-safety specifications, enabling efficient analysis of composite scenarios. Our approach decomposes scenarios into primitives and specifications into sub-specifications, verifies each primitive independently, and composes the resulting statistical estimates using importance sampling and kernel density estimation. Our empirical evaluation shows that the proposed framework can accurately answer verification queries for previously unseen composite scenarios while reducing simulation cost through parallelization and trace reuse.

Abstract

Explore similar work

Scenario-Based Compositional Statistical Model Checking for Safety Specifications

Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes

Beyond F1: Evaluating Coverage and Failure Recovery in AI Model Security Scanners