Wyniki wyszukiwania - BazTech

1

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

Góngora P. A, Rosenblueth D. A.

International Journal of Applied Mathematics and Computer Science

|

2015

|

Vol. 25, no. 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.

2

Wprowadzenie do weryfikacji i symulacji w środowisku NuSMV

Grobelna I.

Metody Informatyki Stosowanej

|

2011

|

nr 1

23-30

PL

Specyfikacja systemu informatycznego jest jednym z pierwszych etapów jego tworzenia i stanowi fundament dalszych prac. Na tym etapie projektu określany jest sposób działania systemu oraz właściwości jego pracy. Należy zadbać o to, aby specyfikacja była w pełni poprawna, a zaprojektowany system spełniał wszystkie stawiane mu wymagania . Jedną z metod walidacji specyfikacji jest weryfikacja oraz symulacja modelu systemu. Oba zadania mogą zostać wykonane w środowisku NuSMV.

EN

The article is a short introduction into model checking and simulation in the NuSMV environment. The NuSMV tool allows description offinite state machines FSM and their verification using temporal logic formulas. Using a simple example (traffic lights), basic rules and commands of model checking and simulation process are presented. Using the NuSMV environment it is possible to detect some errors at an early stage of system development.

3

Automatyczna weryfikacja i synteza regułowego modelu sterownika logicznego

Grobelna I.

Metody Informatyki Stosowanej

|

2011

|

nr 3

59-65

EN

The article focuses on model checking and synthesis of rule-based specification of logic controller. It describes and illustrates proposed design system of logic controllers. Specification by means of Control Interpreted Petri Nets is formally written as rule-based logical model, which is suitable both for formal verification against behavioral requirements and for synthesis in form of reconfigurable logic controller. Verifiable model is thereby consistent with synthesizable model. Logical model is also used for behavioral verification and simulation. Translation process of rule-based specification into verifiable model description and synthesizable code has been automated.

4

A State Transition Model for Honest Executions of Authentication Protocols

Kurkowski M.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2005

|

Vol. 10

83-94

EN

Cryptographic protocols are very good tools to achieve authentication in large distributed computer network. These protocols are precisely defined sequences of actions (communication and computation steps) which use some cryptographic mechanism such as encryption and decryption. It is well known that the design of authentication cryptographic protocols is error prone. Several protocols have been shown flawed in computer security literature. Due to this it is necessary to have some methods of analysis and properties verification of these protocols. It is obvious that in investigations of these properties a suitable formal model is needed. This model should express all important properties and ideas of protocols. Usually size of modeIs introduced by many people is very huge and searching of these modeIs is impossible. In this paper we propose a new formal model of honest executions of cryptographic authentication protocol. To decrease number of states in our model we propose some partial order reduction. We hope that this model is a good startpoint for further investigations and will be usefull in verification of real executions of cryptographic protocols.