- arXiv.org
- Applied Physics
- Popular Physics
- Data Analysis, Statistics and Probability
- Fluid Dynamics
- Optics
- Physics and Society
- Space Physics
- History and Philosophy of Physics
- General Physics
- Biological Physics
- Geophysics
- Plasma Physics
- Atomic Physics
- Atomic and Molecular Clusters
- Medical Physics
- Instrumentation and Detectors
- Computational Physics
- Chemical Physics
- Accelerator Physics
- Classical Physics
- Atmospheric and Oceanic Physics
- Physics Education

- Information Theory
- Analysis of PDEs
- History and Overview
- Number Theory
- Statistics Theory
- Group Theory
- Mathematical Physics
- Representation Theory
- Probability
- Combinatorics
- Algebraic Geometry
- Symplectic Geometry
- Operator Algebras
- Complex Variables
- Geometric Topology
- Differential Geometry
- Metric Geometry
- Optimization and Control
- Logic
- Dynamical Systems
- Numerical Analysis
- Quantum Algebra
- General Topology
- General Mathematics
- K-Theory and Homology
- Functional Analysis
- Spectral Theory
- Classical Analysis and ODEs
- Commutative Algebra
- Algebraic Topology
- Rings and Algebras
- Category Theory

- Neural and Evolutionary Computing
- Information Theory
- General Literature
- Emerging Technologies
- Symbolic Computation
- Mathematical Software
- Learning
- Information Retrieval
- Computer Vision and Pattern Recognition
- Databases
- Programming Languages
- Sound
- Operating Systems
- Formal Languages and Automata Theory
- Multiagent Systems
- Social and Information Networks
- Software Engineering
- Human-Computer Interaction
- Computer Science and Game Theory
- Artificial Intelligence
- Discrete Mathematics
- Cryptography and Security
- Distributed, Parallel, and Cluster Computing
- Hardware Architecture
- Systems and Control
- Numerical Analysis
- Other Computer Science
- Computational Complexity
- Robotics
- Computation and Language
- Data Structures and Algorithms
- Computational Engineering, Finance, and Science
- Logic in Computer Science
- Multimedia
- Performance
- Computational Geometry
- Computers and Society
- Networking and Internet Architecture
- Graphics
- Digital Libraries

- Dec 11 2017 cs.LO arXiv:1712.02872v1Dynamic fault trees (DFTs) have emerged as an important tool for capturing the dynamic behavior of system failure. These DFTs are then analyzed qualitatively and quantitatively using stochastic or algebraic methods to judge the failure characteristics of the given system in terms of the failures of its sub-components. Model checking has been recently proposed to conduct the failure analysis of systems using DFTs with the motivation to provide a rigorous failure analysis of safety-critical systems. However, model checking has not been used for the DFT qualitative analysis and the reduction algorithms used in model checking are usually not formally verified. Moreover, the analysis time grows exponentially with the increase of the number of states. These issues limit the usefulness of model checking for analyzing complex systems used in safety-critical domains, where the accuracy and completeness of analysis matters the most. To overcome these limitations, we propose a comprehensive methodology to perform the qualitative and quantitative analysis of DFTs using an integration of theorem proving and model checking based approaches. For this purpose, we formalized all the basic dynamic fault tree gates using higher-order logic based on the algebraic approach and formally verified some of the simplification properties. This formalization allows us to formally verify the equivalence between the original and reduced DFTs using a theorem prover, and conduct the qualitative analysis. We then use model checking to perform the quantitative analysis of the formally verified reduced DFT. We applied our methodology to five benchmarks and the results show that the formally verified reduced DFT was analyzed using model checking with up to six times less states and up to 133000 times faster.

A Rational Agent Controlling an Autonomous Vehicle: Implementation and Fo...

Martin Henessey Oct 03 2017 01:48 UTCZoltán Zimborás May 28 2014 04:42 UTC

It's a bit funny to look at a formally verified proof of the CLT :), here it is online:

https://github.com/avigad/isabelle.

- Supported by Silverpond.