4 citations · 8 across the 5 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2014
Model Checking Markov Chains Against Unambiguous Buchi Automata
Michael Benedikt, Rastislav Lenhardt, James Worrell
We give a polynomial-time algorithm for model checking finite Markov chains against omega-regular specifications given as unambiguous Buchi automata.
cs.LO2013★ 4 cited
Controlling the Depth, Size, and Number of Subtrees for Two-variable Logic on Trees
Saguy Benaim, Michael Benedikt, Rastislav Lenhardt +1
Verification of properties of first order logic with two variables FO2 has been investigated in a number of contexts. Over arbitrary structures it is known to be decidable with NEX…
cs.LO2013★ 4 cited
Two Variable vs. Linear Temporal Logic in Model Checking and Games
Michael Benedikt, Rastislav Lenhardt, James Worrell
Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In this paper we con…