2020/07/17 by B.C. van Huijgevoort, Sofie Haesaert, van Huijgevoort, B. C. +2 · 1 citation
Biochemistry, Genetics and Molecular Biology · Computer Science · Engineering · #FOS: Electrical engineering #Formal Methods in Verification #Gene Regulatory Network Analysis #Petri Nets in System Modeling #Safety Systems Engineering in Autonomy #Software Reliability and Analysis Research #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2007.09052
openalex publication_date 2020/07/17 · openalex created_date 2022/09/06 · openalex updated_date 2026/08/01
For the formal verification and design of control systems, abstractions with quantified accuracy are crucial. This is especially the case when considering accurate deviation bounds between a stochastic continuous-state model and its finite (reduced-order) abstraction. In this work, we introduce a coupling compensator to parameterize the set of relevant couplings and we give a comprehensive computational approach and analysis for linear stochastic systems. More precisely, we develop a computational method that characterizes the set of possible simulation relations and gives a trade-off between the error contributions on the systems output and deviations in the transition probability. We show the effect of this error trade-off on the guaranteed satisfaction probability for case studies where a formal specification is given as a temporal logic formula.