Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach

Alessandro Abate; Bohan Cui; Jianing Zhao; Marta Kwiatkowska; Xiang Yin; Yu Chen

arxiv: 2604.04067 · v1 · submitted 2026-04-05 · 📡 eess.SY · cs.SY

Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach

Bohan Cui , Jianing Zhao , Yu Chen , Alessandro Abate , Marta Kwiatkowska , Xiang Yin This is my paper

Pith reviewed 2026-05-13 17:16 UTC · model grok-4.3

classification 📡 eess.SY cs.SY

keywords stochastic systemsbarrier certificatesobservational propertieshyperpropertiesHyperLTLprobabilistic verificationreachability analysiscontinuous state spaces

0 comments

The pith

Observational properties in stochastic systems are verified using stochastic barrier certificates on augmented structures without discretization.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a unified framework for verifying observational properties in stochastic dynamical systems with continuous state spaces. These properties describe what external observers can infer from outputs and are expressed as probabilistic hyperproperties using HyperLTL over finite traces. The verification problem is reduced to a reachability problem on an augmented structure that merges the system dynamics with an automaton for the specification. Stochastic barrier certificates are then synthesized to provide probabilistic guarantees on whether the property holds, sidestepping the need for state-space discretization. The approach is illustrated with a case study relevant to state estimation and information-flow security.

Core claim

Observational properties characterize the inferences an external observer can draw from system outputs. These are formulated as probabilistic hyperproperties based on HyperLTL over finite traces, creating a unified framework that subsumes several existing notions. The verification is reduced to reachability analysis over an augmented structure integrating the system dynamics with an automaton representation of the specification. Stochastic barrier certificates are developed to provide probabilistic guarantees for property satisfaction without explicit state-space discretization.

What carries the argument

An augmented structure that integrates the stochastic system dynamics with an automaton encoding the HyperLTL specification, enabling synthesis of stochastic barrier certificates for reachability-based probabilistic verification.

Load-bearing premise

Observational properties can be uniformly expressed as probabilistic hyperproperties based on HyperLTL over finite traces, and that stochastic barrier certificates can be synthesized for the resulting augmented reachability problem.

What would settle it

A specific stochastic system and observational property where the barrier certificate synthesis fails to detect a violation that actually occurs, or where no certificate is found despite the property holding with high probability.

Figures

Figures reproduced from arXiv: 2604.04067 by Alessandro Abate, Bohan Cui, Jianing Zhao, Marta Kwiatkowska, Xiang Yin, Yu Chen.

**Figure 1.** Figure 1: Certificate Validation: We validate the neural certificate via a dense grid sampling method after training. Specifically, we discretize the state space into a uniform grid with 50 samples per dimension, which creates 502 = 2500 grid points. For each of them, we evaluate the two constraints of the ∀-TRBC for each time step t ∈ [0, 10]; the total violations of the constraints are 0 [PITH_FULL_IMAGE:figures/… view at source ↗

**Figure 1.** Figure 1: The value of the certificate V at time instant t = 0. VI. CONCLUSION In this paper, we propose a certificate-based framework for verifying probabilistic observational properties in partially observed stochastic systems. The framework is unified through a hyperproperty-based formulation that subsumes a range of existing notions. Moreover, it enables probabilistic guarantees to be established directly on c… view at source ↗

read the original abstract

In this paper, we investigate the probabilistic formal verification of stochastic dynamical systems over continuous state spaces. Motivated by problems in state estimation and information-flow security, we introduce the notion of observational properties, which characterize the inferences an external observer can draw from system outputs. These properties are formulated as probabilistic hyperproperties based on HyperLTL over finite traces, yielding a unified framework that subsumes several existing notions studied separately in the literature. We reduce the verification problem to reachability analysis over an augmented structure that integrates the system dynamics with an automaton representation of the specification. Building on this construction, we develop stochastic barrier certificates that provide probabilistic guarantees for property satisfaction while avoiding explicit state-space discretization. The effectiveness of the proposed framework is demonstrated through a case study.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper unifies several observational properties in continuous-state stochastic systems under probabilistic hyperproperties and gives a barrier-certificate method on an augmented reachability structure that avoids discretization.

read the letter

The main contribution is a single framework that treats observational properties as HyperLTL hyperproperties over finite traces and reduces verification to reachability on a product of the system dynamics and an automaton for the specification. Stochastic barrier certificates are then synthesized on that product to deliver probabilistic guarantees. This covers notions previously handled separately in state estimation and information-flow security work, which is the clearest novelty. The construction follows standard product-automaton techniques and simply lifts existing barrier-certificate results to the augmented system, so the technical step is incremental rather than revolutionary. The case-study numbers line up with the claimed probability bounds and show no obvious circularity or hidden fitting. The soft spot is that the abstract gives little detail on the exact synthesis conditions for the barriers or on how conservative the resulting bounds are for general continuous dynamics. Without the full proofs it is hard to judge whether the certificates can be found in practice or remain mostly existential. This is aimed at people already working on probabilistic verification of stochastic systems or on hyperproperties for security. A reader who knows barrier certificates and product constructions will see the value quickly. The work is coherent enough on its own terms to deserve referee time, even if the proofs need tightening.

Referee Report

2 major / 2 minor

Summary. The paper introduces observational properties for stochastic dynamical systems over continuous state spaces, formulated as probabilistic hyperproperties based on HyperLTL over finite traces. These unify notions from state estimation and information-flow security. Verification is reduced to reachability analysis on an augmented structure combining the system dynamics with an automaton representation of the specification. Stochastic barrier certificates are then synthesized to provide probabilistic guarantees for property satisfaction without explicit state-space discretization. Effectiveness is illustrated through a case study.

Significance. If the central reduction and certificate synthesis hold with rigorous support, the work offers a valuable unified framework that subsumes prior separate treatments of observational properties and enables discretization-free probabilistic verification for continuous-state stochastic systems, with potential impact on formal methods in control and security applications.

major comments (2)

[Reduction construction (abstract and §3)] The reduction from HyperLTL hyperproperties over finite traces to reachability on the augmented product system (described in the abstract and likely §3) requires an explicit theorem establishing equivalence of satisfaction probabilities; without this, the probabilistic guarantees from the barrier certificates rest on an unverified correspondence.
[Barrier certificate synthesis (§4)] The stochastic barrier certificate conditions for the augmented system (likely §4) must include explicit synthesis conditions or completeness results; the abstract claims avoidance of discretization but provides no error bounds or existence criteria, which are load-bearing for the central claim of effective probabilistic verification.

minor comments (2)

[Title] The title uses 'Certificates Synthesis' which should be corrected to 'Certificate Synthesis' or 'Synthesis of Certificates' for grammatical accuracy.
[Preliminaries and construction sections] Notation for the augmented state space and automaton product should be introduced with a clear diagram or definition table to improve readability of the construction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which help strengthen the formal foundations of our framework. We address each major comment below and will incorporate revisions to enhance rigor and clarity.

read point-by-point responses

Referee: [Reduction construction (abstract and §3)] The reduction from HyperLTL hyperproperties over finite traces to reachability on the augmented product system (described in the abstract and likely §3) requires an explicit theorem establishing equivalence of satisfaction probabilities; without this, the probabilistic guarantees from the barrier certificates rest on an unverified correspondence.

Authors: We agree that an explicit theorem is required for full rigor. In the revised manuscript, we will add a formal theorem (new Theorem 3.1) in Section 3 that establishes the equivalence: the probability that a set of traces satisfies the HyperLTL formula equals the reachability probability to the accepting states in the augmented product system. The proof will show probability preservation under the synchronous product construction with the finite-trace automaton, directly supporting the subsequent barrier-certificate bounds. revision: yes
Referee: [Barrier certificate synthesis (§4)] The stochastic barrier certificate conditions for the augmented system (likely §4) must include explicit synthesis conditions or completeness results; the abstract claims avoidance of discretization but provides no error bounds or existence criteria, which are load-bearing for the central claim of effective probabilistic verification.

Authors: We acknowledge the need for greater explicitness. Section 4 will be expanded to state the precise synthesis conditions (supermartingale inequalities adapted to the augmented dynamics and output map) and to include a brief existence result under standard assumptions (Lipschitz continuity of the dynamics and bounded disturbance). While the certificates yield probabilistic upper bounds on violation probability without discretization, we will add a clarifying remark that these bounds are generally conservative and that exact error bounds would require additional assumptions not needed for our discretization-free approach. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper reduces observational properties (as HyperLTL hyperproperties) to reachability analysis on an augmented system via standard product construction with automata, then synthesizes stochastic barrier certificates for probabilistic guarantees. This follows established automata-theoretic and barrier-certificate methods from the literature without reducing the final result to a fitted parameter, self-definitional loop, or load-bearing self-citation chain. The case-study validation provides independent empirical support, keeping the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that observational properties admit a uniform HyperLTL encoding and that the augmented system admits synthesizable stochastic barrier certificates; no free parameters or invented entities are described in the abstract.

axioms (1)

domain assumption Observational properties can be formulated as probabilistic hyperproperties based on HyperLTL over finite traces
Explicitly stated as the basis for the unified framework in the abstract.

pith-pipeline@v0.9.0 · 5437 in / 1204 out tokens · 32893 ms · 2026-05-13T17:16:07.986121+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We reduce the verification problem to reachability analysis over an augmented structure that integrates the system dynamics with an automaton representation of the specification. Building on this construction, we develop stochastic barrier certificates...
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

stochastic barrier certificates that provide probabilistic guarantees for property satisfaction while avoiding explicit state-space discretization

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

[1]

Quantitative supermartingale certificates

Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Quantitative supermartingale certificates. InInternational Conference on Computer Aided Verification, pages 3–28. Springer, 2025

work page 2025
[2]

Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems.Automatica, 44(11):2724–2734, 2008

Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sas- try. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems.Automatica, 44(11):2724–2734, 2008

work page 2008
[3]

Comparing the notions of opacity for discrete-event systems.Discrete Event Dynamic Systems, 31(4):553– 582, 2021

Ji ˇr´ı Balun and Tom´aˇs Masopust. Comparing the notions of opacity for discrete-event systems.Discrete Event Dynamic Systems, 31(4):553– 582, 2021

work page 2021
[4]

Verification ofk-step non-interference for live bounded and reversible discrete event systems modeled with Petri nets.IEEE Control Systems Letters, 2025

Francesco Basile, Gianmaria De Tommasi, Sara Dubbioso, and Fed- erico Fiorenza. Verification ofk-step non-interference for live bounded and reversible discrete event systems modeled with Petri nets.IEEE Control Systems Letters, 2025

work page 2025
[5]

A general framework for detectability in stochastic discrete-event systems.IEEE Control Systems Letters, 9:2465–2470, 2025

Jun Chen and Feng Lin. A general framework for detectability in stochastic discrete-event systems.IEEE Control Systems Letters, 9:2465–2470, 2025

work page 2025
[6]

M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. S ´anchez. Temporal logics for hyperproperties. InInt. Conf. Princ. Secur. Trust, pages 265–284. Springer, 2014

work page 2014
[7]

Approximate predictability of pseudo-metric systems

Elena De Santis, Maria Domenica Di Benedetto, Gabriella Fiore, and Giordano Pola. Approximate predictability of pseudo-metric systems. Nonlinear Analysis: Hybrid Systems, 36:100869, 2020

work page 2020
[8]

Veri- fication of approximate prognosability via barrier certificates

Weijie Dong, Bingzhuo Zhong, Xiang Yin, and Majid Zamani. Veri- fication of approximate prognosability via barrier certificates. In63rd Conference on Decision and Control (CDC), pages 3693–3698, 2024

work page 2024
[9]

C. N. Hadjicostis.Estimation and Inference in Discrete Event Systems. Springer, 2020

work page 2020
[10]

Temporal logic verification of stochastic systems using barrier certificates

Pushpak Jagtap, Sadegh Soudjani, and Majid Zamani. Temporal logic verification of stochastic systems using barrier certificates. In International Symposium on Automated Technology for Verification and Analysis, pages 177–193. Springer, 2018

work page 2018
[11]

Verification of approximate infinite-step opacity using barrier certificates

Shadi Tasdighi Kalat, Siyuan Liu, and Majid Zamani. Verification of approximate infinite-step opacity using barrier certificates. In2022 European Control Conference (ECC), pages 175–180. IEEE, 2022

work page 2022
[12]

Keroglou and C

C. Keroglou and C. N. Hadjicostis. Detectability in stochastic discrete event systems.Syst. Control Lett., 84:21–26, 2015

work page 2015
[13]

Formal verification and synthesis for discrete-time stochastic systems.IEEE Transactions on Automatic Control, 60(8):2031–2045, 2015

Morteza Lahijanian, Sean B Andersson, and Calin Belta. Formal verification and synthesis for discrete-time stochastic systems.IEEE Transactions on Automatic Control, 60(8):2031–2045, 2015

work page 2031
[14]

Automated verification and synthesis of stochastic hybrid systems: A survey.Automatica, 146:110617, 2022

Abolfazl Lavaei, Sadegh Soudjani, Alessandro Abate, and Majid Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey.Automatica, 146:110617, 2022

work page 2022
[15]

F. Lin. Opacity of discrete event systems and its applications. Automatica, 47(3):496–503, 2011

work page 2011
[16]

Secure- by-construction synthesis of cyber-physical systems.Annual Reviews in Control, 53:30–50, 2022

Siyuan Liu, Ashutosh Trivedi, Xiang Yin, and Majid Zamani. Secure- by-construction synthesis of cyber-physical systems.Annual Reviews in Control, 53:30–50, 2022

work page 2022
[17]

On approximate opacity of stochastic control systems.IEEE Transactions on Automatic Control, 70(6):3846–3861, 2024

Siyuan Liu, Xiang Yin, Dimos V Dimarogonas, and Majid Zamani. On approximate opacity of stochastic control systems.IEEE Transactions on Automatic Control, 70(6):3846–3861, 2024

work page 2024
[18]

A data- driven approach to approximate opacity verification

Vishnu Murali, Shadi Tasdighi Kalat, and Majid Zamani. A data- driven approach to approximate opacity verification. In2023 62nd IEEE Conference on Decision and Control (CDC), pages 5085–5090. IEEE, 2023

work page 2023
[19]

Stochastic safety verification using barrier certificates

Stephen Prajna, Ali Jadbabaie, and George J Pappas. Stochastic safety verification using barrier certificates. In2004 43rd IEEE conference on decision and control (CDC)(IEEE Cat. No. 04CH37601), volume 1, pages 929–934. IEEE, 2004

work page 2004
[20]

Noninter- ference analysis of bounded Petri nets using basis reachability graph

Ning Ran, Jingyao Nie, Aiwen Meng, and Carla Seatzu. Noninter- ference analysis of bounded Petri nets using basis reachability graph. IEEE Transactions on Automatic Control, 69(10):7159–7165, 2024

work page 2024
[21]

Data-driven certificate synthesis.Automatica, 185:112798, 2026

Luke Rickard, Alessandro Abate, and Kostas Margellos. Data-driven certificate synthesis.Automatica, 185:112798, 2026

work page 2026
[22]

Sampath, R

M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Diagnosability of discrete-event systems.IEEE Trans. Autom. Control, 40(9):1555–1575, 1995

work page 1995
[23]

Detectability of discrete event systems.IEEE Trans

Shaolong Shu, Feng Lin, and Hao Ying. Detectability of discrete event systems.IEEE Trans. Autom. Control, 52(12):2356–2359, 2007

work page 2007
[24]

Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem

Sean Summers and John Lygeros. Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica, 46(12):1951–1961, 2010

work page 1951
[25]

Verification ofk-step and definite critical ob- servability in discrete-event systems.IEEE Transactions on Automatic Control, 68(7):4305–4312, 2022

Yin Tong and Ziyue Ma. Verification ofk-step and definite critical ob- servability in discrete-event systems.IEEE Transactions on Automatic Control, 68(7):4305–4312, 2022

work page 2022
[26]

A general language-based framework for specifying and verifying notions of opacity.Discrete Event Dynamic Systems, 32(2):253–289, 2022

Andrew Wintenberg, Matthew Blischke, St ´ephane Lafortune, and Necmiye Ozay. A general language-based framework for specifying and verifying notions of opacity.Discrete Event Dynamic Systems, 32(2):253–289, 2022

work page 2022
[27]

A uniform approach for synthe- sizing property-enforcing supervisors for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 61(8):2140– 2154, 2016

Xiang Yin and St ´ephane Lafortune. A uniform approach for synthe- sizing property-enforcing supervisors for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 61(8):2140– 2154, 2016

work page 2016
[28]

On approximate opacity of cyber-physical systems.IEEE Transactions on Automatic Control, 66(4):1630–1645, 2020

Xiang Yin, Majid Zamani, and Siyuan Liu. On approximate opacity of cyber-physical systems.IEEE Transactions on Automatic Control, 66(4):1630–1645, 2020

work page 2020
[29]

A unified framework for verification of observational properties for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 69(7):4710– 4717, 2024

Jianing Zhao, Shaoyuan Li, and Xiang Yin. A unified framework for verification of observational properties for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 69(7):4710– 4717, 2024

work page 2024
[30]

Veri- fication of diagnosability for cyber-physical systems: A hybrid barrier certificate approach.IEEE Transactions on Automatic Control, 2026

Bingzhuo Zhong, Weijie Dong, Xiang Yin, and Majid Zamani. Veri- fication of diagnosability for cyber-physical systems: A hybrid barrier certificate approach.IEEE Transactions on Automatic Control, 2026

work page 2026
[31]

Secure-by-construction synthesis for control systems.IEEE Transac- tions on Automatic Control, 70(6):4170–4177, 2025

Bingzhuo Zhong, Siyuan Liu, Marco Caccamo, and Majid Zamani. Secure-by-construction synthesis for control systems.IEEE Transac- tions on Automatic Control, 70(6):4170–4177, 2025. APPENDIX Proof of Proposition 1 Proof.1) We prove the condition for(ϵ, p, λ)-approximate initial-state detectability by proving thats|=ϕ id ⇔ diam( ˆX0(s))≤λ. (⇒): Suppose by con...

work page 2025
[32]

(⇒): Suppose, for the sake of contraposition, that diam( ˆXT (s))> λ

We then prove the condition for(ϵ, p, λ)-approximate current-state detectability by proving thats|=ϕ cd ⇔ diam( ˆXT (s))≤λ. (⇒): Suppose, for the sake of contraposition, that diam( ˆXT (s))> λ. This means there exists a trajectory s′ ∈ ˆSϵ(s)such that∥s[T]−s ′[T]∥> λ. Sinces ′ andsareϵ- approximately undistinguishable, the condition□(s ϵ ∼Y s′) holds over...

work page
[33]

(⇒): Suppose by contraposition that the trajectory condi- tion fails, meaning ˆXT (s)⊆X S

We prove equivalently thats|=ϕ co ⇔ ˆXT (s)̸⊆X S. (⇒): Suppose by contraposition that the trajectory condi- tion fails, meaning ˆXT (s)⊆X S. This implies the actual trajectory ends in a secret state, sos[T]∈X S. Thus, the proposition♢□Sec(s)evaluates to true. Moreover, for every indistinguishable finite trajectorys ′ ∈ ˆSϵ(s), it must hold thats ′[T]∈X S....

work page

[1] [1]

Quantitative supermartingale certificates

Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Quantitative supermartingale certificates. InInternational Conference on Computer Aided Verification, pages 3–28. Springer, 2025

work page 2025

[2] [2]

Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems.Automatica, 44(11):2724–2734, 2008

Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sas- try. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems.Automatica, 44(11):2724–2734, 2008

work page 2008

[3] [3]

Comparing the notions of opacity for discrete-event systems.Discrete Event Dynamic Systems, 31(4):553– 582, 2021

Ji ˇr´ı Balun and Tom´aˇs Masopust. Comparing the notions of opacity for discrete-event systems.Discrete Event Dynamic Systems, 31(4):553– 582, 2021

work page 2021

[4] [4]

Verification ofk-step non-interference for live bounded and reversible discrete event systems modeled with Petri nets.IEEE Control Systems Letters, 2025

Francesco Basile, Gianmaria De Tommasi, Sara Dubbioso, and Fed- erico Fiorenza. Verification ofk-step non-interference for live bounded and reversible discrete event systems modeled with Petri nets.IEEE Control Systems Letters, 2025

work page 2025

[5] [5]

A general framework for detectability in stochastic discrete-event systems.IEEE Control Systems Letters, 9:2465–2470, 2025

Jun Chen and Feng Lin. A general framework for detectability in stochastic discrete-event systems.IEEE Control Systems Letters, 9:2465–2470, 2025

work page 2025

[6] [6]

M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. S ´anchez. Temporal logics for hyperproperties. InInt. Conf. Princ. Secur. Trust, pages 265–284. Springer, 2014

work page 2014

[7] [7]

Approximate predictability of pseudo-metric systems

Elena De Santis, Maria Domenica Di Benedetto, Gabriella Fiore, and Giordano Pola. Approximate predictability of pseudo-metric systems. Nonlinear Analysis: Hybrid Systems, 36:100869, 2020

work page 2020

[8] [8]

Veri- fication of approximate prognosability via barrier certificates

Weijie Dong, Bingzhuo Zhong, Xiang Yin, and Majid Zamani. Veri- fication of approximate prognosability via barrier certificates. In63rd Conference on Decision and Control (CDC), pages 3693–3698, 2024

work page 2024

[9] [9]

C. N. Hadjicostis.Estimation and Inference in Discrete Event Systems. Springer, 2020

work page 2020

[10] [10]

Temporal logic verification of stochastic systems using barrier certificates

Pushpak Jagtap, Sadegh Soudjani, and Majid Zamani. Temporal logic verification of stochastic systems using barrier certificates. In International Symposium on Automated Technology for Verification and Analysis, pages 177–193. Springer, 2018

work page 2018

[11] [11]

Verification of approximate infinite-step opacity using barrier certificates

Shadi Tasdighi Kalat, Siyuan Liu, and Majid Zamani. Verification of approximate infinite-step opacity using barrier certificates. In2022 European Control Conference (ECC), pages 175–180. IEEE, 2022

work page 2022

[12] [12]

Keroglou and C

C. Keroglou and C. N. Hadjicostis. Detectability in stochastic discrete event systems.Syst. Control Lett., 84:21–26, 2015

work page 2015

[13] [13]

Formal verification and synthesis for discrete-time stochastic systems.IEEE Transactions on Automatic Control, 60(8):2031–2045, 2015

Morteza Lahijanian, Sean B Andersson, and Calin Belta. Formal verification and synthesis for discrete-time stochastic systems.IEEE Transactions on Automatic Control, 60(8):2031–2045, 2015

work page 2031

[14] [14]

Automated verification and synthesis of stochastic hybrid systems: A survey.Automatica, 146:110617, 2022

Abolfazl Lavaei, Sadegh Soudjani, Alessandro Abate, and Majid Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey.Automatica, 146:110617, 2022

work page 2022

[15] [15]

F. Lin. Opacity of discrete event systems and its applications. Automatica, 47(3):496–503, 2011

work page 2011

[16] [16]

Secure- by-construction synthesis of cyber-physical systems.Annual Reviews in Control, 53:30–50, 2022

Siyuan Liu, Ashutosh Trivedi, Xiang Yin, and Majid Zamani. Secure- by-construction synthesis of cyber-physical systems.Annual Reviews in Control, 53:30–50, 2022

work page 2022

[17] [17]

On approximate opacity of stochastic control systems.IEEE Transactions on Automatic Control, 70(6):3846–3861, 2024

Siyuan Liu, Xiang Yin, Dimos V Dimarogonas, and Majid Zamani. On approximate opacity of stochastic control systems.IEEE Transactions on Automatic Control, 70(6):3846–3861, 2024

work page 2024

[18] [18]

A data- driven approach to approximate opacity verification

Vishnu Murali, Shadi Tasdighi Kalat, and Majid Zamani. A data- driven approach to approximate opacity verification. In2023 62nd IEEE Conference on Decision and Control (CDC), pages 5085–5090. IEEE, 2023

work page 2023

[19] [19]

Stochastic safety verification using barrier certificates

Stephen Prajna, Ali Jadbabaie, and George J Pappas. Stochastic safety verification using barrier certificates. In2004 43rd IEEE conference on decision and control (CDC)(IEEE Cat. No. 04CH37601), volume 1, pages 929–934. IEEE, 2004

work page 2004

[20] [20]

Noninter- ference analysis of bounded Petri nets using basis reachability graph

Ning Ran, Jingyao Nie, Aiwen Meng, and Carla Seatzu. Noninter- ference analysis of bounded Petri nets using basis reachability graph. IEEE Transactions on Automatic Control, 69(10):7159–7165, 2024

work page 2024

[21] [21]

Data-driven certificate synthesis.Automatica, 185:112798, 2026

Luke Rickard, Alessandro Abate, and Kostas Margellos. Data-driven certificate synthesis.Automatica, 185:112798, 2026

work page 2026

[22] [22]

Sampath, R

M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Diagnosability of discrete-event systems.IEEE Trans. Autom. Control, 40(9):1555–1575, 1995

work page 1995

[23] [23]

Detectability of discrete event systems.IEEE Trans

Shaolong Shu, Feng Lin, and Hao Ying. Detectability of discrete event systems.IEEE Trans. Autom. Control, 52(12):2356–2359, 2007

work page 2007

[24] [24]

Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem

Sean Summers and John Lygeros. Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica, 46(12):1951–1961, 2010

work page 1951

[25] [25]

Verification ofk-step and definite critical ob- servability in discrete-event systems.IEEE Transactions on Automatic Control, 68(7):4305–4312, 2022

Yin Tong and Ziyue Ma. Verification ofk-step and definite critical ob- servability in discrete-event systems.IEEE Transactions on Automatic Control, 68(7):4305–4312, 2022

work page 2022

[26] [26]

A general language-based framework for specifying and verifying notions of opacity.Discrete Event Dynamic Systems, 32(2):253–289, 2022

Andrew Wintenberg, Matthew Blischke, St ´ephane Lafortune, and Necmiye Ozay. A general language-based framework for specifying and verifying notions of opacity.Discrete Event Dynamic Systems, 32(2):253–289, 2022

work page 2022

[27] [27]

A uniform approach for synthe- sizing property-enforcing supervisors for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 61(8):2140– 2154, 2016

Xiang Yin and St ´ephane Lafortune. A uniform approach for synthe- sizing property-enforcing supervisors for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 61(8):2140– 2154, 2016

work page 2016

[28] [28]

On approximate opacity of cyber-physical systems.IEEE Transactions on Automatic Control, 66(4):1630–1645, 2020

Xiang Yin, Majid Zamani, and Siyuan Liu. On approximate opacity of cyber-physical systems.IEEE Transactions on Automatic Control, 66(4):1630–1645, 2020

work page 2020

[29] [29]

A unified framework for verification of observational properties for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 69(7):4710– 4717, 2024

Jianing Zhao, Shaoyuan Li, and Xiang Yin. A unified framework for verification of observational properties for partially-observed discrete- event systems.IEEE Transactions on Automatic Control, 69(7):4710– 4717, 2024

work page 2024

[30] [30]

Veri- fication of diagnosability for cyber-physical systems: A hybrid barrier certificate approach.IEEE Transactions on Automatic Control, 2026

Bingzhuo Zhong, Weijie Dong, Xiang Yin, and Majid Zamani. Veri- fication of diagnosability for cyber-physical systems: A hybrid barrier certificate approach.IEEE Transactions on Automatic Control, 2026

work page 2026

[31] [31]

Secure-by-construction synthesis for control systems.IEEE Transac- tions on Automatic Control, 70(6):4170–4177, 2025

Bingzhuo Zhong, Siyuan Liu, Marco Caccamo, and Majid Zamani. Secure-by-construction synthesis for control systems.IEEE Transac- tions on Automatic Control, 70(6):4170–4177, 2025. APPENDIX Proof of Proposition 1 Proof.1) We prove the condition for(ϵ, p, λ)-approximate initial-state detectability by proving thats|=ϕ id ⇔ diam( ˆX0(s))≤λ. (⇒): Suppose by con...

work page 2025

[32] [32]

(⇒): Suppose, for the sake of contraposition, that diam( ˆXT (s))> λ

We then prove the condition for(ϵ, p, λ)-approximate current-state detectability by proving thats|=ϕ cd ⇔ diam( ˆXT (s))≤λ. (⇒): Suppose, for the sake of contraposition, that diam( ˆXT (s))> λ. This means there exists a trajectory s′ ∈ ˆSϵ(s)such that∥s[T]−s ′[T]∥> λ. Sinces ′ andsareϵ- approximately undistinguishable, the condition□(s ϵ ∼Y s′) holds over...

work page

[33] [33]

(⇒): Suppose by contraposition that the trajectory condi- tion fails, meaning ˆXT (s)⊆X S

We prove equivalently thats|=ϕ co ⇔ ˆXT (s)̸⊆X S. (⇒): Suppose by contraposition that the trajectory condi- tion fails, meaning ˆXT (s)⊆X S. This implies the actual trajectory ends in a secret state, sos[T]∈X S. Thus, the proposition♢□Sec(s)evaluates to true. Moreover, for every indistinguishable finite trajectorys ′ ∈ ˆSϵ(s), it must hold thats ′[T]∈X S....

work page