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. |
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 |