Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 2

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych:  model checking
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

Component composition validation

100%
Speck A., Pulvermüller E., Jerger M., Franczyk B.
International Journal of Applied Mathematics and Computer Science
|
2002
|
tom 12
|
nr 4
581-589
EN
Many approaches such as component technologies have been invented in order to support software reuse. Based on these technologies a large variety of techniques have been introduced to connect components. However, there is little experience concerning the validation of component systems. We know how to plug components together, but we do need ways to check whether that works. In this paper we introduce an approach to validating component compositions and showing how such a process can be supported by tools. We introduce a way to compare the interface specification of components automatically against the code. Furthermore, we demonstrate how compositions of components can be specified by logical formulas, allowing us to automatically validate these compositions.
2
Artykuł dostępny w postaci pełnego tekstu - kliknij by otworzyć plik
Content available

A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria

88%
Góngora P., Rosenblueth D.
International Journal of Applied Mathematics and Computer Science
|
2015
|
tom 25
|
nr 3
577-596
EN
Consider games where players wish to minimize the cost to reach some state. A subgame-perfect Nash equilibrium can be regarded as a collection of optimal paths on such games. Similarly, the well-known state-labeling algorithm used in model checking can be viewed as computing optimal paths on a Kripke structure, where each path has a minimum number of transitions. We exploit these similarities in a common generalization of extensive games and Kripke structures that we name “graph games”. By extending the Bellman-Ford algorithm for computing shortest paths, we obtain a model-checking algorithm for graph games with respect to formulas in an appropriate logic. Hence, when given a certain formula, our model-checking algorithm computes the subgame-perfect Nash equilibrium (as opposed to simply determining whether or not a given collection of paths is a Nash equilibrium). Next, we develop a symbolic version of our model checker allowing us to handle larger graph games. We illustrate our formalism on the critical-path method as well as games with perfect information. Finally, we report on the execution time of benchmarks of an implementation of our algorithms.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.