SiSAT
Subproject | H1/2 |
Categories | Core algorithms, Model checker / solver for probabilistic systems, Model checker / solver for hybrid systems |
Overview | SiSAT is a solver for stochastic satisfiability modulo theories (SSMT) problems. The notion of SSMT extends satisfiability modulo theories problems with randomized (stochastic) as well as existential and universal quantification as known from stochastic propositional satisfiability (SSAT). SiSAT supports non-linear arithmetic over the reals and integers involving transcendental functions. It can also be used as a bounded model checker for discrete-time probabilistic hybrid (discrete-continuous) systems. |
T. Teige, A. Eggers, and M. Fränzle. Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. Nonlinear Analysis: Hybrid Systems, 5(2):343-366, 2011. M. Fränzle, T. Teige, and A. Eggers. Satisfaction meets expectations: Computing expected values of probabilistic hybrid systems with SMT. In Dominique Mery and Stephan Merz, editors, Integrated Formal Methods 2010, volume 6396 of Lecture Notes in Computer Science (LNCS), pages 168-182. Springer-Verlag, 2010. M. Fränzle, T. Teige, and A. Eggers. Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. Journal of Logic and Algebraic Programming, 79:436-466, 2010. T. Teige and M. Fränzle. Constraint-based analysis of probabilistic hybrid systems. In A. Giua, C. Mahulea, M. Silva, and J. Zaytoon, editors, Proceedings of the 3rd International IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009), pages 162-167, 2009. M. Fränzle, H. Hermanns, and T. Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Magnus Egerstedt and Bud Mishra, editors, Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08), volume 4981 of Lecture Notes in Computer Science (LNCS), pages 172-186, 2008. T. Teige and M. Fränzle. Stochastic satisfiability modulo theories for non-linear arithmetic. In L. Perron and M. A. Trick, editors, 5th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, volume 5015 of Lecture Notes in Computer Science (LNCS), pages 248-262, 2008. | |
Networked Automation System, Networked Control System | |
Download | See SiSAT website at projects.avacs.org. |
Manual | See SiSAT website at projects.avacs.org. |
Status | Stable |