@article{cleaveland_iyer_narasimha_2005, title={Probabilistic temporal logics via the modal mu-calculus}, DOI={10.1016/j.tcs.2005.03.048}, abstractNote={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) “systems” and (nonprobabilistic) “observations”: 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.}, number={03-Feb}, journal={Theoretical Computer Science}, author={Cleaveland, Rance and Iyer, S. Purushothaman and Narasimha, Murali}, year={2005}, month={Apr} }
 @inbook{narasimha_cleaveland_iyer_1999, title={Probabilistic temporal logics via the modal mu-calculus}, volume={1578}, ISBN={3540657193}, booktitle={Foundations of software science and computation structures: Second International Conference, FOSSACS '99 held as part of the joint European Conferences on Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999: proceedings}, publisher={Berlin; New York: Springer}, author={Narasimha, M. and Cleaveland, R. and Iyer, P.}, year={1999}, pages={288–305} }
 @article{cleaveland_dayar_smolka_yuen_1999, title={Testing Preorders for Probabilistic Processes}, DOI={10.1006/inco.1999.2808}, abstractNote={We present a testing preorder for probabilistic processes based on a quantification of the probability with which processes pass tests. The theory enjoys close connections with the classical testing theory of De Nicola and Hennessy in that whenever a process passes a test with probability 1 (respectively some nonzero probability) in our setting, then the process must (respectively may) pass the test in the classical theory. We also develop an alternative characterization of the probabilistic testing preorders that takes the form of a mapping from probabilistic traces to the interval [0, 1], where a probabilistic trace is an alternating sequence of actions and probability distributions over actions. Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.}, number={2}, journal={Information and Computation}, author={Cleaveland, Rance and Dayar, Zeynep and Smolka, Scott A. and Yuen, Shoji}, year={1999}, month={Nov} }
 @article{cleaveland_lüttgen_natarajan_1998, title={A process algebra with distributed priorities}, DOI={10.1016/S0304-3975(97)00221-1}, abstractNote={This paper presents a process algebra for distributed systems in which some actions may take precedence over others. The algebra is distinguished by the design decision that it only allows actions to pre-empt others at the same “location” and therefore captures a notion of localized precedence . Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence and present logical characterizations of our behavioral relations. Simple examples highlight the utility of the theory.}, number={2}, journal={Theoretical Computer Science}, author={Cleaveland, Ranee and Lüttgen, Gerald and Natarajan, V.}, year={1998}, month={Mar} }
 @article{elseaidy_cleaveland_baugh_1997, title={Modeling and verifying active structural control systems}, volume={29}, DOI={10.1016/S0167-6423(96)00031-7}, abstractNote={This paper presents the results of a case study involving the use of a formal graphical notation, Modechart, and an automatic verification tool, the Concurrency Workbench, in the analysis of the design of a fault-tolerant active structural control system. Such control systems must satisfy strict requirements on their timing behavior; we show how to use various equivalence-based features supported by the Workbench to examine the timing behavior of different design alternatives, one of which has in excess of 1019 states. The central insight arising from the study involves the importance of compositionality for reasoning about large and complex systems; in particular, the success of the case study depends integrally on our notation's and tool's support of componentwise minimization.}, number={1-2}, journal={Science of Computer Programming}, author={Elseaidy, Wael M. and Cleaveland, Rance and Baugh, John W.}, year={1997}, month={Jul}, pages={99–122} }