Specifying coalgebras with modal logic

We propose to use modal logic as a logic for coalgebras and discuss it in view of the work done on coalgebras as a semantics of object-oriented programming. Two approaches are taken: First, standard concepts of modal logic are applied to coalgebras. For a certain kind of functor it is shown that the logic exactly captures the notion of bisimulation and a complete calculus is given. Examples of verifications of object properties are given. Second, we discuss the relationship of this approach with the coalgebraic logic of Moss (Coalgebraic logic, Ann Pure Appl. Logic 96 (1999) 277–317.).     

The ‘Cash-Point’ Service: A Verification Case Study Using STeP

STeP, the Stanford Temporal Prover, supports the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [MBB99]. Automated model checking is combined with computer-aided deductive methods to allow for the verification of a broad class of systems, including parameterised (N-component) circuit designs, parameterised (N-process) programs, and programs with infinite data domains. Received February 2000 / Accepted in revised form December 2000     

The Cash-Point Service in NUT

This paper describes how the cash-point service can be modelled and simulated using the NUT system. Received February 2000 / Accepted in revised form December 2000     

From liveness to promptness

Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the “wait time” for an eventuality to be fulfilled. That is, F θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as designers tend to interpret an eventuality F θ as an abstraction of a bounded eventuality F ^≤k θ, for an unknown k, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here prompt-LTL, an extension of LTL with the prompt-eventually operator F _p . A system S satisfies a prompt-LTL formula φ if there is some bound k on the wait time for all prompt-eventually subformulas of φ in all computations of S. We study various problems related to prompt-LTL, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques that are quite close to the standard techniques for LTL.     

Specifying real-time properties in autonomic systems

Increasingly, computer software must adapt dynamically to changing conditions. The correctness of adaptation cannot be rigorously addressed without precisely specifying the requirements for adaptation. In many situations, these requirements involve absolute time, in addition to a logical ordering of events. This paper introduces an approach to formally specifying such timing requirements for adaptive software. We introduce TA-LTL, a timed adaptation-based extension to linear temporal logic, and use this logic to specify three timing properties associated with the adaptation process: safety, liveness, and stability. A dynamic adaptation scenario involving interactive audio streaming software is used to illustrate the timed temporal logic. A number of related papers and technical reports of the Software Engineering and Network Systems Laboratory can be found at the following URL: http://www.cse.msu.edu/sens.     

Expressiveness of propositional projection temporal logic with star

This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω-regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes.     

A general technique for proving lock-freedom

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.     

Specification,proof, and model checking of the Mondex electronic purse using RAISE

This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering. J. C. P. Woodcock     

Deciding safety and liveness in TPTL

We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented by Sistla [1] to decide the corresponding problems for LTL.     

CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks

Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for genetic regulatory networks (Grns). Applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties (needed for specifying multistability and oscillation properties, respectively). At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this paper, we define Computation Tree Regular Logic (Ctrl), an extension of Ctl with regular expressions and fairness operators that attempts to match these criteria. Ctrl subsumes both Ctl and Ltl, and has a reduced set of temporal operators indexed by regular expressions. We also develop a translation of Ctrl into Hennessy-Milner Logic with Recursion (HmlR), an equational variant of the modal μ-calculus. This has allowed us to obtain an on-the-fly model checker with diagnostic for Ctrl by directly reusing the verification technology available in the Cadp toolbox. We illustrate the application of the Ctrl model checker by analyzing the Grn controlling the carbon starvation response of Escherichia coli.     

Model checking for a probabilistic branching time logic with fairness

We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic choice between probability distributions. These systems can be decomposed into a collection of “computation trees” which arise by resolving the non-deterministic, but not probabilistic, choices. The presence of non-determinism means that certain liveness properties cannot be established unless fairness is assumed. We introduce a probabilistic branching time logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL [14]. The formulas of the logic express properties such as “every request is eventually granted with probability at least p”. We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time quantifiers are taken to range over a certain kind of fair computation trees. We then present a model checking algorithm for verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We also propose adaptations of existing model checking algorithms for pCTL [4, 14] to obtain procedures for PBTL under fairness constraints. The techniques developed in this paper have applications in automatic verification of randomized distributed systems. Received: June 1997 / Accepted: May 1998     

Einstein谜的SAT求解

Einstein谜,亦称Zebra谜,是爱因斯坦在20世纪初提出的,他说世界上有98%的人答不出来。该问题是一个典型的逻辑推理题,可以通过SAT求解给出问题的答案。现将Einstein谜转换成SAT求解问题,并使用当前流行的SAT求解器,如MinSat,对Einstein谜进行自动求解。     

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .     

Specifying safety-critical systems with a decidable duration logic

Punctual timing constraints are important in formal modelling of safety-critical real-time systems. But they are very expensive to express in dense time. In most cases, punctuality and dense-time lead to undecidability. Efforts have been successful to obtain decidability; but the results are either non-primitive recursive or nonelementary. In this paper we propose a duration logic which can express quantitative temporal constraints and punctuality timing constraints over continuous intervals and has a reasonable complexity. Our logic allows most specifications that are interesting in practice, and retains punctuality. It can capture the semantics of both events and states, and incorporates the notions duration and accumulation. We call this logic ESDL (the acronym stands for Event- and State-based Duration Logic). We show that the satisfiability problem is decidable, and the complexity of the satisfiability problem is NEXPTIME. ESDL is one of a few decidable interval temporal logics with metric operators. Through some case studies, we also show that ESDL can specify many safety-critical real-time system properties which were previously specified by undecidable interval logics or their decidable reductions based on some abstractions.     

Composing and Refining Dense Temporal Logic Specifications

A dense temporal logic development method for the specification, refinement, composition and verification of reactive systems is introduced. A reactive system is specified by a pair consisting of a machine and a condition that indicate the valid computations of this machine. Compositionality is achieved by indicating whether each step is an environment step, a system step, or a communication step. Refinement can be expressed straightforwardly in the logic because the stutter problem is elegantly solved by using the dense structure of the logic. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The latter can then be verified by existing proof rules for refinement which are reformulated in our formalism. Received January 1997 / Accepted in revised form April 2000     

Specifying modules to satisfy interfaces: A state transition system approach

Summary We defineinterface, module and the meaning ofM offers I, whereM denotes a module andI an interface. For a moduleM and disjoint interfacesU andL, the meaning ofM using L offers U is also defined. For a linear hierarchy of modules and interfaces,M ₁, I₁, M₂, I₂, ...,M _n, I_n, we present the following composition theorem: IfM ₁ offersI ₁ and, fori=2, ...,n, M _i usingI _i–1 offersI _i, then the hierarchy of modules offersI _n.Our theory is applied to solve a problem posed by Leslie Lamport at the 1987 Lake Arrowhead Workshop. We first present a formal specification of a serializable database interface. We then provide specifications of two modules, one based upon two-phase locking and the other multi-version timestamps; the two-phase locking module uses an interface offered by a physical database. We prove that each module offers the serializable interface. Simon S. Lam is Chairman of the Department of Computer Sciences at the University of Texas at Austin and holds and endowed professorship. His research interests are in the areas of computer networks, communication protocols, performance models, formal methods, and network security. He serves on the editorial boards ofIEEE Transactions on Software Engineering andPerformance Evaluation. He is an IEEE Fellow, and was a corecipient of the 1975 Leonard G. Abraham Prize Paper Award from the IEEE Communications Society. He organized and was program chairman of the first ACM SIGCOMM Symposium on Communications Architectures and Protocols in 1983. He received the BSEE degree (with Distinction) from Washington State University in 1969, and the MS and Ph.D. degrees from the University of California at Los Angeles in 1970 and 1974 respectively. Prior to joining the University of Texas faculty, he was with the IBM T.J. Watson Research Center from 1974 to 1977. A. Udaya Shankar received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, Kanpur, in 1976, the M.S. degree in Computer Engineering from Syracuse University, Syracuse, NY, in 1978, and the Ph.D. degree in Electrical Engineering from the University of Texas at Austin, in 1982. Since January 1983, he has been with the University of Maryland, College Park, where he is now an Associate Professor of Computer Science. Since September 1985, he has been with the Institute for Advanced Computer Studies at the University of Maryland. His current research interests include the modeling and analysis of distributed systems and network protocols, from both correctness and performance aspects. He is a member of IEEE and ACM.The work of Simon S. Lam was supported by National Science Foundation grants no. NCR-8613338 and no. NCR-9004464. The work of A. Udaya Shankar was supported by National Science Foundation grants no. ECS-8502113 and no. NCR-8904590     

Specification and refinement of mobile systems in MTLA and mobile UML

We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics.     

Petri net based verification of distributed algorithms: An example

A technique to model and to verify distributed algorithms is suggested. This technique (based on Petri nets) reduces the modelling and analysis effort to a reasonable level. The paper outlines the technique using the example of a typical network algorithm, theecho algorithm.Supported by the DFG-projects Verteilte Algorithmen and Konsensalgorithmen