Wyniki wyszukiwania - BazTech

1

Additional Winning Strategies in Reachability Games

Malvone V., Murano A., Sorrentino L.

Fundamenta Informaticae

|

2018

|

Vol. 159, nr 1/2

175--195

EN

In game theory, deciding whether a designed player wins a game amounts to check whether he has a winning strategy. However, there are several game settings in which knowing whether he has more than a winning strategy is also important. For example, this is crucial in deciding whether a game admits a unique Nash Equilibrium, or in planning a rescue as this would provide a backup plan. In this paper we study the problem of checking whether, in a two-player reachability game, a designed player has more than a winning strategy. We investigate this question both under perfect and imperfect information about the moves performed by the players. We provide an automata-based solution that results, in the perfect information setting, in a linear-time procedure; in the imperfect information setting, instead, it shows an exponential-time upper bound. In both cases, the results are tight.

2

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.

3

Dynamic network functional comparison via approximate-bisimulation

Donnarumma F., Murano A., Prevete R.

Control and Cybernetics

|

2015

|

Vol. 44, no. 1

99--127

EN

It is generally unknown how to formally determine whether diﬀerent neural networks have a similar behaviour. This question intimately relates to the problem of ﬁnding a suitable similarity measure to identify bounds on the input-output response distances of neural networks, which has several interesting theoretical and computational implications. For example, it can allow one to speed up the learning processes by restricting the network parameter space, or to test the robustness of a network with respect to parameter variation. In this paper we develop a procedure that allows for comparing neural structures among them. In particular, we consider dynamic networks composed of neural units, characterised by non-linear diﬀerential equations, described in terms of autonomous continuous dynamic systems. The comparison is established by importing and adapting from the formal veriﬁcation setting the concept of δ−approximate bisimulations techniques for non-linear systems. We have positively tested the proposed approach over continuous time recurrent neural networks (CTRNNs).