LiQuor: A tool for Qualitative and Quantitative Linear Time analysis of Reactive Systems

LiQuor is a tool for verifying probabilistic reactive systems modelled Probmela programs, which are terms of a probabilistic guarded command language with an operational semantics based on (finite) Markov decision processes. LiQuor provides the facility to perform a qualitative or quantitative analysis for ω-regular linear time properties by means of automata-based model checking algorithms.

• Type: Conference
• Year: 2006
• Where: QEST
• Authors: Frank Ciesinski, Christel Baier
• Keywords: Markov Decision Processes, Probabilistic Guarded Command, Probabilistic Reactive Systems, QEST 2006, Quantitative Evaluation Of Systems