@ARTICLE{Rataj_Artur_Translation_2013,
 author={Rataj, Artur},
 volume={vol. 25},
 number={No 3-4},
 journal={Theoretical and Applied Informatics},
 pages={157-182},
 howpublished={online},
 year={2013},
 publisher={Committee of Informatics of Polish Academy of Science},
 publisher={Institute of Theoretical and Applied Informatics of Polish Academy of Science},
 abstract={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.},
 type={Article},
 title={Translation of probabilistic games in J2TADD},
 URL={http://journals.pan.pl/Content/116278/PDF-MASTER/Rataj_Translation_of_Probabilistic_Games.pdf},
 keywords={model checking, Java, probabilistic game},
}