Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system into its functional components and code each as an isolated and encapsulated system. Our goal is to help bringing compositionality to system specification in rewriting logic. The base of our proposal is the operation that we call synchronous composition. We discuss the motivations and implications of our proposal, formalize it for rewriting logic and also for transition structures, to be used as semantics, and show the power of our approach with some examples. This paper is under consideration in Theory and Practice of Logic Programming (TPLP).
Plain TLR*, as described in @cite_25 , stays a step away from our goal, because transitions are given by proof terms, that univocally determine one origin state and one destination state for each transition. TLR* uses proof-term patterns (called ), that are used literally in temporal formulas. The problem is that, in this way, a TLR* formula is tied to a particular algebraic specification (one in which the pattern makes sense). In contrast, an LTL or CTL formula is meaningful by itself and can be used on any system specification by using atomic proposition definitions as interfaces. Notably, propositions on transitions have been added to plain TLR*, in some way or another, in all the implementations of model checkers for (the linear-time subset of) TLR* that we are aware of @cite_36 @cite_51 @cite_14 @cite_9 . None of them, however, tries to allow a same proposition to be defined both in states and in transitions, which we need for flexible synchronization.
@cite_14 @cite_36 @cite_9 @cite_51 @cite_25
2109187338 2151284417 2167672803 1986424898
Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. We present a generalization of the branching-time logic CTL which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. In every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ¬ determine sup and inf over all paths from a given state, and the temporal operators ♦ and □ specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path.We interpret the resulting logic DCTL over transition systems, Markov chains, and Markov decision processes. We present two semantics for DCTL: a path semantics, inspired by the standard interpretation of state and path formulas in CTL, and a fixpoint semantics, inspired by the µ-calculus evaluation of CTL formulas. We show that, while these semantics coincide for CTL, they differ for DCTL, and we provide model-checking algorithms for both semantics. This paper presents a model checker for LTLR, a subset of the temporal logic of rewriting TLR* extending linear temporal logic with spatial action patterns. Both LTLR and TLR* are very expressive logics generalizing well-known state-based and action-based logics. Furthermore, the semantics of TLR* is given in terms of rewrite theories, so that the concurrent systems on which the LTLR properties are model checked can be specified at a very high level with rewrite rules. This paper answers a nontrivial challenge, namely, to be able to build a model checker to model check LTLR formulas on rewrite theories with relatively little effort by reusing [email protected]?s LTL model checker for rewrite theories. For this, the reflective features of both rewriting logic and its Maude implementation have proved extremely useful. We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics. We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one. In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm. This paper presents the linear temporal logic of rewriting (LTLR) model checker under localized fairness assumptions for the Maude system. The linear temporal logic of rewriting extends linear temporal logic (LTL) with spatial action patterns that describe patterns of rewriting events. Since LTLR generalizes and extends various state-based and event-based logics, mixed properties involving both state propositions and actions, such as fairness properties, can be naturally expressed in LTLR. However, often the needed fairness assumptions cannot even be expressed as propositional temporal logic formulas because they are parametric, that is, they correspond to universally quantified temporal logic formulas. Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness is localized to the object name parameter in object fairness conditions. We summarize the foundations, and present the language design and implementation of the Maude Fair LTLR model checker, developed at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our tool provides not only an efficient LTLR model checking algorithm under parameterized fairness assumptions but also suitable specification languages as part of its user interface. The expressiveness and effectiveness of the Maude Fair LTLR model checker are illustrated by five case studies. This is the first tool we are aware of that can model check temporal logic properties under parameterized fairness assumptions. We develop the LTLR model checker under localized fairness assumptions.The linear temporal logic of rewriting (LTLR) extends LTL with action patterns.Localized fairness specifies parameterized fairness over generic system entities.We present the foundations, the language design, and the implementation of our tool.We illustrate the expressiveness and effectiveness of our tool with case studies.