@inproceedings{NokovicSekerinski13pState,
	title = {{pState}: {A} {Probabilistic} {Statecharts} {Translator}},
	doi = {10.1109/MECO.2013.6601339},
	abstract = {We describe pState, an experimental so ware toolkit for the design, validation and formal veri cation of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems. Costs/rewards can be used to compute quantitative properties such as expected power consumption or expected number of lost messages in model of some communication protocol. State invariants are used to express safety conditions or consistency constraints. The charts are validated and transformed into an intermediate representation, from which code for various languages can be generated.},
	booktitle = {Embedded {Computing} ({MECO}), 2nd {Mediterranean} {Conference} on},
	publisher = {IEEE Press},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Stojanović, Radovan and Jóźwiak, Lech and Lutovac, Budimir},
	month = jun,
	year = {2013},
	keywords = {Computational modeling, invariants, model-checking, quantitative properties, statecharts, verification},
	pages = {29--32},
}

{"_id":"ya6Yqkr9dAwDw6XHR","bibbaseid":"nokovic-sekerinski-pstateaprobabilisticstatechartstranslator-2013","author_short":["Nokovic, B.","Sekerinski, E."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"pState: A Probabilistic Statecharts Translator","doi":"10.1109/MECO.2013.6601339","abstract":"We describe pState, an experimental so ware toolkit for the design, validation and formal veri cation of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems. Costs/rewards can be used to compute quantitative properties such as expected power consumption or expected number of lost messages in model of some communication protocol. State invariants are used to express safety conditions or consistency constraints. The charts are validated and transformed into an intermediate representation, from which code for various languages can be generated.","booktitle":"Embedded Computing (MECO), 2nd Mediterranean Conference on","publisher":"IEEE Press","author":[{"propositions":[],"lastnames":["Nokovic"],"firstnames":["Bojan"],"suffixes":[]},{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Stojanović"],"firstnames":["Radovan"],"suffixes":[]},{"propositions":[],"lastnames":["Jóźwiak"],"firstnames":["Lech"],"suffixes":[]},{"propositions":[],"lastnames":["Lutovac"],"firstnames":["Budimir"],"suffixes":[]}],"month":"June","year":"2013","keywords":"Computational modeling, invariants, model-checking, quantitative properties, statecharts, verification","pages":"29–32","bibtex":"@inproceedings{NokovicSekerinski13pState,\n\ttitle = {{pState}: {A} {Probabilistic} {Statecharts} {Translator}},\n\tdoi = {10.1109/MECO.2013.6601339},\n\tabstract = {We describe pState, an experimental so ware toolkit for the design, validation and formal veri cation of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems. Costs/rewards can be used to compute quantitative properties such as expected power consumption or expected number of lost messages in model of some communication protocol. State invariants are used to express safety conditions or consistency constraints. The charts are validated and transformed into an intermediate representation, from which code for various languages can be generated.},\n\tbooktitle = {Embedded {Computing} ({MECO}), 2nd {Mediterranean} {Conference} on},\n\tpublisher = {IEEE Press},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Stojanović, Radovan and Jóźwiak, Lech and Lutovac, Budimir},\n\tmonth = jun,\n\tyear = {2013},\n\tkeywords = {Computational modeling, invariants, model-checking, quantitative properties, statecharts, verification},\n\tpages = {29--32},\n}\n\n","author_short":["Nokovic, B.","Sekerinski, E."],"editor_short":["Stojanović, R.","Jóźwiak, L.","Lutovac, B."],"key":"NokovicSekerinski13pState","id":"NokovicSekerinski13pState","bibbaseid":"nokovic-sekerinski-pstateaprobabilisticstatechartstranslator-2013","role":"author","urls":{},"keyword":["Computational modeling","invariants","model-checking","quantitative properties","statecharts","verification"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"],"keywords":["computational modeling","invariants","model-checking","quantitative properties","statecharts","verification"],"search_terms":["pstate","probabilistic","statecharts","translator","nokovic","sekerinski"],"title":"pState: A Probabilistic Statecharts Translator","year":2013}