Wyniki wyszukiwania - BazTech

1

On Promptness in Parity Games

Mogavero F., Murano A., Sorrentino L.

Fundamenta Informaticae

|

2015

|

Vol. 139, nr 3

277--305

EN

Parity games are infinite-duration two-player turn-based games that provide powerful formal-method techniques for the automatic synthesis and verification of distributed and reactive systems. This kind of game emerges as a natural evaluation technique for the solution of the μ- calculus model-checking problem and is closely related to alternating ω-automata. Due to these strict connections, parity games are a well-established environment to describe liveness properties such as “every request that occurs infinitely often is eventually responded”. Unfortunately, the classical form of such a condition suffers from the strong drawback that there is no bound on the effective time that separates a request from its response, i.e., responses are not promptly provided. Recently, to overcome this limitation, several variants of parity game have been proposed, in which quantitative requirements are added to the classic qualitative ones. In this paper, we make a general study of the concept of promptness in parity games that allows to put under a unique theoretical framework several of the cited variants along with new ones. Also, we describe simple polynomial reductions from all these conditions to either Büchi or parity games, which simplify all previous known procedures. In particular, they allow to lower the complexity class of cost and bounded-cost parity games recently introduced. Indeed, we provide solution algorithms showing that determining the winner of these games is in UPTIME ∩ COUPTIME.

2

On Modal μ-Calculus in S5 and Applications

D'Agostino G., Lenzi G.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

465--482

EN

We consider the μ-calculus over graphs where the accessibility relation is an equivalence (S5-graphs). We show that the vectorial μ-calculus model checking problem over arbitrary graphs reduces to the vectorial, existential μ-calculus model checking problem over S5 graphs. Moreover, we give a proof that satisfiability of μ-calculus in S5 is NP-complete, and by using S5 graphs we give a new proof that the satisfiability problem of the existential μ-calculus is also NP-complete. Finally we prove that on multimodal S5, in contrast with the monomodal case, the fixpoint hierarchy of the μ-calculus is infinite and the finite model property fails.

3

Efficient Algorithms for Games Played on Trees with Back-edges

Gandhi A., Khoussainov B., Liu J.

Fundamenta Informaticae

|

2011

|

Vol. 111, nr 4

391-412

EN

This paper studies algorithms for deciding the winners of two-player games played on directed graphs. We focus on the case when the underlying graphs are trees with back-edges and provide both theoretical and experimental analysis of this class of games. In particular, we present an algorithm that solves Büchi games played on trees with back-edges in time O(min{r źm, l+m}) where m is the number of edges, l is the sum of the distances from the root to all leaves and the parameter r is bounded by the height of the tree. We also show that parity games played on trees with back-edges can be solved in time O(l + m).

4

A Linear Time Special Case for MC Games

Poranen T., Nummenmaa J.

Fundamenta Informaticae

|

2002

|

Vol. 50, nr 3,4

315-324

EN

MC games are infinite duration two-player games played on graphs. Deciding the winner in MC games is equivalent to the the modal mu-calculus model checking. In this article we provide a linear time algorithm for a class of MC games. We show that, if all cycles in each strongly connected component of the game graph have at least one common vertex, the winner can be found in linear time. Our results hold also for parity games, which are equivalent to MC games.