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

Abstract

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.