Translation of probabilistic games in J2TADD

• Autorzy: Rataj A.

Warianty tytułu

PL

Translacja gier probabilistycznych w J2TADD

• Języki publikacji: EN

Abstrakty

EN

A new version of J2TADD - a translator from Java to automatons- is described, which adds support for a translation of Markov processes with non-dcterministic players, that can form coalitions, which in turn strive for different aims. In order to ease the definition of a probabilistic game using a plain Java application, several new constructs, and also a special library, are supported within the input language.Ranges on variables or on expressions can be defined, what helps in checking the self-consistency of a model, and can also make the solving of the model faster.

PL

Artykuł prezentuje nową wersję translatora J2TADD. Dodane zostało tłumaczenie procesów markowowskich z niedelerministycznymi graczami, mogącymi formować koalicje mające różne cele. By ułatwić pisanie gier probabilistycznych dodane zostało kilka specyficznych dla gier konstrukcji, jak również specjalna biblioteka. Aktualnej wersja posiada również kilka innych usprawnień: ● wybory, które są zwykłymi wyrażeniami języka Java, jednak hc tłumaczy je na specyficzne dla automatów rozgałęzienia probabilistyczne lub niedeterministyczne; ● można definiować dopuszczalne wartości zmiennych, co pomaga w sprawdzaniu wewnętrznej spójności modelu, a także może przyspieszyć jego rozwiązanie; ● różne metody specyfikacji niezmienników i warunków zegarowych. Artykuł prezentuje jako przykład prostą grę probabilistyczną, modelującą rynek lokalnego dostawcy energii elektrycznej. W ramach przykładu omawiane są wersje automatów do rozwiązywania metodą analityczną i symulacyjną.

Słowa kluczowe

EN

model checking; Java; probabilistic game

• Wydawca: Instytut Informatyki Teoretycznej i Stosowanej Polskiej Akademii Nauk
• Czasopismo: Theoretical and Applied Informatics
• Rocznik: 2013
• Tom: Vol. 25, No. 3-4
• Strony: 157--182
• Opis fizyczny: Bibliogr. 7 poz., rys.

Twórcy

autor

Rataj A.

• U'l'iS PAN, Bałtycka 5, Gliwice, Poland

Bibliografia

• [1] Gerd Behrmann, Alexandre David, and Kim G. Larsen. A tutorial on UPPAAL. In Lecture Notes in Computer Science, volume 3185, pages 200-236. Springer, 2004.
• [2] H. Hildmann and F. Saffre. Influence of variable supply and load flexibility on demand-side management. In Proc. 8th International Conference on the European Energy Market (EEM’11), pages 63-68, 2011.
• [3] M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. 23rd International Conference on Computer Aided Verification (CAV’ll), volume 6806 of LNCS, pages 585-591. Springer, 2011.
• [4] M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang. Symbolic model checking for probabilistic timed automata. In Y. Lakhnech and S. Yovine, editors, Proc. Joint Conference on Fonnal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant Systems (FORMATS/FTRTFT'04), volume 3253 of LNCS, pages 293-308. Springer, 2004.
• [5] D. Peled. Ten years of partial order reduction. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 17-28. Springer Berlin Heidelberg, 1998.
• [6] A. Rataj. More flexible models using a new version of the translator of Java sources to timed automatons J2TADD. Theoretical and Applied Informatics, 21 (2): 107-114, 2009.
• [7] A. Rataj, B. Wozna, and A. Zbrzezny. A translator of Java programs to TADDs. In Concurrency; Specification and Programming (CS&P 2008), pages 524-535, Gross Vaeter near Berlin, Germany, 2008.