ABSTRACT. Passive learning of formal models from observed system behavior has produced a rich body of results for sequential computational models. Extending this success to concurrent systems poses fundamental new challenges: concurrent models are more succinct, often lack a unique minimal representative, and their semantics depends on the interplay of multiple simultaneous processes. A common restriction in prior work on learning of concurrent models is the assumption of a fixed, known number of processes---an assumption that is fundamentally at odds with parametrized systems, which are designed to operate correctly for any number of processes. We summarize our recent work on passive learning of broadcast protocols (BPs), a well-studied model of parametrized concurrent systems. For the class of fine BPs--BPs with no hidden state and a finite cutoff--we establish a comprehensive learnability picture: a constraint-based passive learning algorithm that infers a BP consistent with a given sample, returning a minimal equivalent BP when the sample subsumes a characteristic set; hardness results showing that consistency is NP-complete, that characteristic set may be exponentially large, and that fine BPs are not polynomially predictable; along side LeoParDS, the first tool implementing theses techniques in the parametrized setting.

ABSTRACT. We present TPTND-Lean, a Lean 4 implementation of a core fragment of Trustworthy Probabilistic Typed Natural Deduction (TPTND). TPTND-Lean type-checks TPTND derivation trees whose leaves are empirical observations, and whose internal nodes are introduction or elimination rules for probabilistic connectives, producing machine-checked fairness certificates. In this implementation, frequencies and stored interval endpoints are rational numbers; the standard-error term used by the score-test acceptance bands is computed via a bounded-rational Newton iteration. The kernel is small and auditable; each derivation it accepts is a transferable, re-checkable certificate that binds together counts, statistical test, band, and verdict in a single typed tree. We describe a four-stage workflow that takes group-level summary statistics through claim selection and derivation construction to such a certificate. Two case studies on public data illustrate the approach: (i) the ProPublica COMPAS recidivism data (6172 defendants, reproducing the headline racial-bias finding), and (ii) HMDA mortgage-lending data for Delaware (54000 Black/White applications across 2022-2023, demonstrating multi-year temporal composition via Update and intersectional comparisons). Certificates are conditional: they verify the derivation relative to the supplied counts, the chosen statistical rule, and the checker, not the upstream data pipeline. The full source, data pipelines, and all derivations are publicly available at https://github.com/dasaro/tptnd-lean.

ABSTRACT. Runtime Monitoring (RM) enables the automated and objective evaluation of a system w.r.t its system specification. In the automotive domain, RM allows for the evaluation of whether a vehicle's actual behaviour corresponds to an abstract specification of its expected behaviour while interacting inside a traffic scenario. Such runtime monitors, in the automotive domain, must not only consider spatial aspects such as distances, positions, velocities, etc., but also temporal aspects such as the order in which particular traffic situations (or scenarios) occur. Existing runtime monitors provide verdicts on whether the actual vehicle behaviour corresponds to the abstract scenario specification, with possible outcomes being satisfied, violated, or inconclusive. Undesired behavior is detected whenever there is a discrepancy between the monitor's verdict and the expected outcome defined by the scenario specification. Tracing the cause for the undesired behaviour requires knowledge of prior system behaviour. This information can be derived from exact knowledge of the intermediate verdicts of the runtime monitor, the so called monitor progression. This is not trivial to determine because the current satisfied constraints may simultaneously correspond to multiple (traffic) situations. Additionally, the satisfaction of temporal properties also depends on prior spatial and temporal properties. To improve the analysis of unexpected system behaviours, we propose progress-aware RM of abstract scenario specifications. Specifically, we introduce hypercuts to describe all non-violating past and future system behaviors, simplifying the analysis of unexpected verdicts. Each monitor verdict is annotated with a hypercut, which allows the samples to be related back to the abstract scenario specification structure. In this work, we provide a well-defined hypercut using Duration Calculus and describe the construction of a progress-aware runtime monitor, based on Traffic Sequence Chart (TSC) monitoring. Finally, we demonstrate how hypercuts improve the analysis of unexpected verdicts through an application example and present a visualization method.

ABSTRACT. Although the integration of machine learning into safety‑critical systems is growing, a fundamental tension remains: performance‑oriented techniques such as parallelism and optimized execution can introduce opacity and nondeterminism, while safety‑critical systems demand transparency and reproducibility. This paper provides a formalization of ONNX computation graphs that addresses these requirements by focusing on the abstract modeling and verification of graph‑based machine learning representations. The proposed workflow, developed within the SONNX initiative, combines the exploration and validation of structural properties of the graph using the Alloy Analyzer — used to explore and validate structural properties via model checking — with a subsequent refinement of the model in the Why3 verifier, enabling deductive reasoning over type invariants and functional properties. We further introduce an execution semantics for the graph model, defined as a state machine where graph configurations correspond to states and node execution induces state transitions. Overall, our proposed model is thus defined as a set of well-formed graph configurations equipped with a single-rule, transition relation.

ABSTRACT. For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components—a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle—a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.

ABSTRACT. Deep reinforcement learning produced adversarial agents capable of superhuman performance. The opacity of these policies creates critical barriers to auditability. Conventional distillation methods make this worse; by focusing on replicating teacher-replay data, they sacrifice robustness at the learner-induced decision frontier—the very states where interpretability matters most. To address this, we introduce an Auditable Composite Distillation on a Sparse Tactical Frontier (AIRD), a composite-policy framework that decomposes these regimes. AIRD employs a human-interpretable nominal tree to govern routine states and a model checking step handles frontier states for introducing residual corrective policy. This architectural separation resolves distribution mismatch at a structural level, eliminating the need for retraining. As a first testbed, we audit Connect4 5x6 environment and show that AIRD extends the safe planning horizon from 8 to 10 play and reduces opponent-attractor states by 47%.

ABSTRACT. Neural networks for vision are widely used but do not provide explanations for their decisions. A recent approach (e.g., ConSpec) uses concepts to bridge the gap between pixel-like features and human-understandable text, and a propositional logic to express specifications of the model's behavior. However, such approach remains limited and cannot express simple properties involving multiple concepts, predicate on their strength (a proxy for the presence of a concept in the input), or predicate on multiple input images. This limitation is mostly due to the non-linear relationship between concepts' strengths and the latent space representation of the model, which makes satisfiability checking difficult and restricts the application of the logic to explain the network's decisions. We propose Concept Parts Network (ConPNet), a novel architecture that integrates the concepts' strengths computation directly into a classifier and then uses these strengths for prediction. Such architecture allows us to extend ConSpec to support arbitrary linear combinations of concepts' strengths (ConSpecReal), which are necessary to express a wider range of specifications, and efficiently check them with an SMT solver. Our initial experiments show that ConPNet retains competitive classification efficiency and supports effective explanation of predictions through ConSpecReal formulas.