SPASS-FPTA

 

Subproject

S2

Categories

Model reduction, Model checker / solver for probabilistic systems, Theorem prover for hybrid systems

Overview

SPASS-FPTA is actually a toolchain that automatically proves reachability properties for First-Order Probabilistic Times Automata (FPTA). It includes SPASS(LA), translation procedures from FPTA into FOL(LA), and from FOL(LA) proofs back into PTA with Boolean variables as well as the mcpta model-checker out of the Modest Toolset.

Publications

A. Fietzke, H. Hermanns, and C. Weidenbach. Superposition-based analysis of first-order probabilistic timed automata. In Christian G. Fermüller and Andrei Voronkov, editors, LPAR-17: 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 6397 of Lecture Notes in Computer Science (LNCS), pages 302-316, 2010.

Benchmarks

Download

---

Manual

---

Status

Proof of Concept