System design of stochastic models using robustness of temporal properties

DOI10.1016/j.tcs.2015.02.046zbMath1327.68147MaRDI QIDQ2348023

Ezio Bartocci, Luca Bortolussi, Guido Sanguinetti, Laura Nenzi

Publication date: 10 June 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.02.046

zbMATH Keywords

stochastic models; temporal logic; system design; robustness degree

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

92C42: Systems biology, networks

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

Unnamed Item, Digital Bifurcation Analysis of Internet Congestion Control Protocols, Parameter Synthesis Through Temporal Logic Specifications, Smoothed model checking for uncertain continuous-time Markov chains, Active and sparse methods in smoothed model checking, Abstract model repair for probabilistic systems, A survey of challenges for runtime verification from advanced application domains (beyond software), Risk verification of stochastic systems with neural network controllers, Spatial Logic and Spatial Model Checking for Closure Spaces

Uses Software

• PRISM
• S-TaLiRo
• BIOCHAM
• Breach
• PRMLT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Robustness of temporal logic specifications for continuous-time signals
• Parametric probabilistic transition systems for system design and analysis
• Transactions on Computational Systems Biology VI
• Formal methods for computational systems biology. 8th international school on formal methods for the design of computer, communication, and software systems, SFM 2008 Bertinoro, Italy, June 2--7, 2008. Advanced lectures
• Hybrid dynamics of stochastic programs
• PRMLT
• How to recognize zero?
• Bayesian Calibration of Computer Models
• (Hybrid) automata and (stochastic) programs * The hybrid automata lattice of a stochastic program
• Mining requirements from closed-loop control models
• Temporal logic inference for classification and prediction from data
• SpaTeL
• S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
• Model Repair for Probabilistic Systems
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Robust Sampling for MITL Specifications
• Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes
• Robust Satisfaction of Temporal Logic over Real-Valued Signals
• The benefits of relaxing punctuality
• Symbolic model checking for probabilistic processes
• On Temporal Logic and Signal Processing
• Multiple Verification in Complex Biological Systems: The Bone Remodelling Case Study
• Computability and Representations of the Zero Set
• Information-Theoretic Regret Bounds for Gaussian Process Optimization in the Bandit Setting
• Tools and Algorithms for the Construction and Analysis of Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Data-Driven Statistical Learning of Temporal Logic Properties
• Hybrid Systems: Computation and Control
• Essentials of Stochastic Processes
• Analog property checkers: a DDR2 case study
• Stochastic differential equations. An introduction with applications.