Logical Foundations of Cyber-Physical Systems

DOI10.1007/978-3-319-63588-0zbMath1400.93003OpenAlexW2885880873MaRDI QIDQ4689064

André Platzer

Publication date: 12 October 2018

Full work available at URL: https://zenodo.org/record/4457120

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Automated systems (robots, etc.) in control theory (93C85) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Other applications of logic (03B80) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to systems and control theory (93-01)

Related Items (31)

Relational Differential Dynamic Logic ⋮ Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Verification of Hybrid Systems ⋮ Adding proof calculi to epistemic logics with structured knowledge ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Logics for actor networks: a two-stage constrained-hybridisation approach ⋮ Verifying Switched System Stability With Logic ⋮ Review of Logical Analysis of Hybrid Systems ⋮ A dynamic logic with branching modalities ⋮ On proving that an unsafe controller is not proven safe ⋮ Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs ⋮ Synthesis of parametric hybrid automata from time series ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ From post-conditions to post-region invariants ⋮ Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems ⋮ Unnamed Item ⋮ Deductive stability proofs for ordinary differential equations ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Towards physical hybrid systems ⋮ Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow ⋮ Book review of: A. Platzer, Logical foundations of cyber-physical systems ⋮ Epistemic logics with structured knowledge ⋮ Constructive hybrid games ⋮ Learning explanations for biological feedback with delays using an event calculus ⋮ Implicit definitions with differential equations for KeYmaera X (system description) ⋮ Notes on Recent Achievements in Proving Stability using KeYmaeraX ⋮ A Survey on Analog Models of Computation ⋮ Moded and continuous abstract state machines

This page was built for publication: Logical Foundations of Cyber-Physical Systems