@article {12769,
	title = {Probabilistic temporal logics via the modal mu-calculus},
	journal = {Theoretical Computer Science},
	volume = {342},
	year = {2005},
	month = {2005/09/07/},
	pages = {316 - 350},
	abstract = {This paper presents a mu-calculus-based modal logic for describing properties of reactive probabilistic labeled transition systems (RPLTSs) and develops a model-checking algorithm for determining whether or not states in finite-state RPLTSs satisfy formulas in the logic. The logic is based on the distinction between (probabilistic) {\^a}{\texteuro}{\oe}systems{\^a}{\texteuro} and (nonprobabilistic) {\^a}{\texteuro}{\oe}observations{\^a}{\texteuro}: using the modal mu-calculus, one may specify sets of observations, and the semantics of our logic then enable statements to be made about the measures of such sets at various system states. The logic may be used to encode a variety of probabilistic modal and temporal logics; in addition, the model-checking problem for it may be reduced to the calculation of solutions to systems of non-linear equations. Finally, the logic induces an equivalence on RPLTSs that coincides with accepted notions of probabilistic bisimulation in the literature.},
	keywords = {Model-checking, Probabilistic bisimulation, Probabilistic temporal logic, Probabilistic transition systems, reactive systems},
	isbn = {0304-3975},
	doi = {10.1016/j.tcs.2005.03.048},
	url = {http://www.sciencedirect.com/science/article/pii/S0304397505001829},
	author = {Cleaveland, Rance and Iyer,S. Purushothaman and Narasimha,Murali}
}
@conference {16336,
	title = {Specification-based Testing of Reactive Software: Tools and Experiments},
	booktitle = {Software Engineering, International Conference on},
	year = {1997},
	month = {1997///},
	pages = {525 - 525},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Los Alamitos, CA, USA},
	abstract = {Testing commercial software is expensive and time consuming. Automated testing methods promise to save a great deal of time and money throughout the software industry. One approach that is well-suited for the reactive systems found in telephone switching systems is specification-based testing.We have built a set of tools to automatically test softmare applications for violations of safety properties expressed in temporal logic. Our testing system automatically constructs finite state machine oracles corresponding to safety properties, builds test harnesses, and integrates them with the application. The test harness then generates inputs automatically to test the application.We describe a study examining the feasibility of this approach for testing industrial applications. To conduct this study we formally modeled an Automatic Protection Switching system (APS), which is an application common to many telephony systems. We then asked a number of computer science graduate students to develop several versions of the APS and use our tools to test them. We found that the tools are very effective, save significant amounts of human effort (at the expense of machine resources), and are easy to use. We also discuss improvements that are needed before we can use the tools with professional developers building commercial products.},
	keywords = {empirical studies, reactive systems, specification-based testing, temporal logic},
	doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.1997.610373},
	author = {Jagadeesan,Lalita Jategaonkar and Porter, Adam and Puchol,Carlos and Ramming,J. Christopher and Votta,Lawrence G.}
}
