Search

• < Previous
• 1
• Next >

---

Antichains for the Automata-Based Approach to Model-Checking

Laurent Doyen ; Jean-Francois Raskin.

We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be&nbsp;[&hellip;]

---

Expressiveness and Closure Properties for Quantitative Languages

Krishnendu Chatterjee ; Laurent Doyen ; Thomas A Henzinger.

Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages~$L$ that assign to each word~$w$ a real number~$L(w)$. In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit-average,&nbsp;[&hellip;]

---

Algorithms for Omega-Regular Games with Imperfect Information

Krishnendu Chatterjee ; Laurent Doyen ; Thomas A. Henzinger ; Jean-Francois Raskin.

We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller&nbsp;[&hellip;]

---

Stochastic Processes with Expected Stopping Time

Krishnendu Chatterjee ; Laurent Doyen.

Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward&nbsp;[&hellip;]

---