29 citations · 149 across the 31 of their papers we have counts for
17 papers · 1 filter
Scenario Approach for Parametric Markov Models
Ying Liu, Andrea Turrini, Moritz Hahn +2
In this paper, we propose an approximating framework for analyzing parametric Markov models. Instead of computing complex rational functions encoding the reachability probability a…
Finding polynomial loop invariants for probabilistic programs
Yijun Feng, Lijun Zhang, David N. Jansen +2
Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing…
Distribution-based bisimulation for labelled Markov processes
Pengfei Yang, David N. Jansen, Lijun Zhang
In this paper we propose a (sub)distribution-based bisimulation for labelled Markov processes and compare it with earlier definitions of state and event bisimulation, which both on…
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
Ernst Moritz Hahn, Sven Schewe, Andrea Turrini +1
2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached…
Verify LTL with Fairness Assumptions Efficiently
Yong Li, Lei Song, Yuan Feng +1
This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness…
An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties
Yong Li, Wanwei Liu, Andrea Turrini +2
In this paper, we propose an efficient algorithm for the parameter synthesis of PLTL formulas with respect to parametric Markov chains. The PLTL formula is translated to an almost…
Extending Hybrid CSP with Probability and Stochasticity
Yu Peng, Shuling Wang, Naijun Zhan +1
Probabilistic and stochastic behavior are omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of fundamental properties of…
A Simple Probabilistic Extension of Modal Mu-calculus
Wanwei Liu, Lei Song, Ji Wang +1
Probabilistic systems are an important theme in AI domain. As the specification language, the logic PCTL is now the default logic for reasoning about probabilistic properties. In t…
LTLf satisfiability checking
Jianwen Li, Lijun Zhang, Geguang Pu +2
We consider here Linear Temporal Logic (LTL) formulas interpreted over \emph{finite} traces. We denote this logic by LTLf. The existing approach for LTLf satisfiability checking is…
Probably Safe or Live
Joost-Pieter Katoen, Lei Song, Lijun Zhang
This paper presents a formal characterisation of safety and liveness properties à la Alpern and Schneider for fully probabilistic systems. As for the classical setting, it is estab…
Fast LTL Satisfiability Checking by SAT Solvers
Jianwen Li, Geguang Pu, Lijun Zhang +2
Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of…
Polsat: A Portfolio LTL Satisfiability Solver
Jianwen Li, Geguang Pu, Lijun Zhang +3
In this paper we present a portfolio LTL-satisfiability solver, called Polsat. To achieve fast satisfiability checking for LTL formulas, the tool integrates four representative LTL…
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
Yuan Feng, Lijun Zhang
Probabilistic automata were introduced by Rabin in 1963 as language acceptors. Two automata are equivalent if and only if they accept each word with the same probability. On the ot…
Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes
Lei Song, Lijun Zhang, Jens Chr. Godskesen
In this paper we study strong and weak bisimulation equivalences for continuous-time Markov decision processes (CTMDPs) and the logical characterizations of these relations with re…
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
Lei Song, Lijun Zhang, Jens Chr. Godskesen +1
Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, wher…
Efficient CSL Model Checking Using Stratification
Lijun Zhang, David N. Jansen, Flemming Nielson +1
For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal,…
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand +1
Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilisti…