unambiguous automata
There is some work on the branch adl/unambiguous
, however it has never been merged (I don't remember why) and needs to be updated to the current code base.
The paper we should cite (if not already done) is "LTL Model Checking of Interval Markov Chains", Michael Benedikt, Rastislav Lenhardt, James Worrell. TACAS'13.