- R. Cleaveland, S.P. Iyer and M. Narasimha
- Probabilistic Temporal Logics via the Modal Mu-Calculus
- In
*Theoretical Computer Science*, 342(2-3):316-350, 7 September 2005. - ©2005 Elsevier.

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.

- B. Sengupta and R. Cleaveland.
- Executable Requirements Specifications using Triggered Message Sequence Charts.
- In D. Chakraborty, editor,
*Second International Conference on Distributed Computing and Internet Technology (ICDCIT 2005)*, volume 3816 of*Lecture Notes in Computer Science*, pages 482-493, Bhubaneswar, India, December 2005. - ©2005 Springer Verlag.

Triggered Message Sequence Charts (TMSCs) are a scenario-based visual formalism for early stage requirements specifications of distributed systems. In this paper, we present a formal operational semantics for TMSCs that allow the simulation of TMSC system descriptions, so that errors and inconsistencies in specification may be detected early on. The semantics is defined in terms of Structured Operational Semantics (SOS) rules that guide the step-wise execution of TMSC specifications. We also consider the equivalence of this semantics and the TMSC denotational semantics that has been presented in previous work.

- D. Zhang and R. Cleaveland
- Fast Generic Model-Checking for Data-Based Systems
- In F. Wang, editor,
*Formal Techniques for Networked and Distributed Systems - FORTE 2005*, volume 3731 of*Lecture Notes in Computer Science*, pages 83-97, Taipei, Taiwan, October 2005. - ©2005 Springer Verlag.

This paper shows how *predicate equation systems* (PESs) may be
used to solve model-checking problems for systems, such as those
involving real-time or value passing, that manipulate data. PESs are first
defined and the encoding of model-checking
problems described; then generic global and local approaches for solving
PESs are given. Real-time model checking is then
considered in detail, and a new, efficient on-the-fly technique for
real-time model checking based on proof search in PESs is developed
and experimentally shown to significantly outperform existing approaches
when system specifications or formula specifications contain errors
and to be competitive when both are correct.

- D. Zhang and R. Cleaveland
- Efficient Temporal-Logic Query Checking for Presburger Systems
- In T. Elman and A. Zisman, editors,
*20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005)*, pages 24-33, Long Beach, California, November 2005. IEEE Computer Society Press. - ©2005 IEEE.

This paper develops a framework for solving temporal-logic query-checking problems for a class of in finite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-logic query-checking problem may be formulated as follows: given a model and a temporal logic formula with placeholders, compute a set of assignments of formulas to placeholders such that the resulting temporal formula is satisfied by the given model. Temporal-logic query checking has proved useful as a means for requirements and design understanding; existing work, however, has focused only on propositional temporal logic and finite-state systems.

Our method is based on a symbolic model-checking technique that relies on proof search. The paper first introduces this model-checking approach and then shows how it can be adapted to solving the temporal queries in which formulas may contain integer variables. We also present experimental results showing the computational efficacy of our approach.

- D. Zhang and R. Cleaveland
- Fast On-The-Fly Parametric Real-Time Model Checking.
- In
*The 26th IEEE Real-Time Systems Symposium (RTSS 2005)*, pages 157-166, Miami, Florida, December 2005. IEEE Computer Society Press. - ©2005 IEEE.

This paper presents a local algorithm for solving the universal parametric real-time model-checking problem. The problem may be phrased as follows: given a real-time system and temporal formula, both of which may contain parameters, and a constraint over the parameters, does every allowed parameter assignment ensure that the real-time system satisfies the formula? Our approach relies on translating these model-checking problems into predicate equation systems, and then using an efficient proof-search algorithm to solve these systems. Experimental data shows that our method substantially outperforms existing approaches for systems that contain errors, while exhibiting comparable behavior for systems that are correct. This fast error-detection capability of our technique makes it especially interesting for design approaches in which model checkers are used "early and often" to detect design errors in an ongoing manner.

Rance Cleaveland Last modified: Thu Oct 26 15:38:31 Eastern Daylight Time 2006