Search

Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past (LTL+P) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response LTL+P ( LTL EBR + P for short) has been introduced. It allows one to express safety languages definable in LTL+P and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce GR-EBR , an extension of LTL EBR + P with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of LTL EBR + P in practice. Second, we the expressiveness of GR-EBR starting from the expressiveness of its fragments. In particular, we prove that: (1) LTL EBR + P is expressively complete with respect to the safety fragment of LTL+P , (2) the removal of past operators from LTL EBR + P results into a loss of expressive power, and (3) GR-EBR is expressively equivalent to the logic GR(1) of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from GR-EBR specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) LTL+P. The experimental evaluation shows promising results. [ABSTRACT FROM AUTHOR]

We study temporal multi-agent logics using a new approach to defining time for individual agents. It is assumed that in any time state each agent (in a sense) generates its own future time, which will only be available for analysis in the future. That is, the defined time interval depends both on the agent and on the initial state where the agent starts to act. It is also assumed that the agent may have intervals of forgotten (lost) time. We investigate problems of unification and problems of computable recognizing admissible inference rules. An algorithm is found for solving these problems based on the construction of a finite computable set of formulas which is a complete set of unifiers. We use the technique of projective formulas developed by S. Ghilardi. It is proved that any unifiable formula is in fact projective and an algorithm is constructed which creates its projective unifier. Thereby we solve the unification problem, and based at this, find the solution to the open problem of computable recognizing admissible inference rules. [ABSTRACT FROM AUTHOR]

Although universities promote undergraduate degrees as journeys of exploration and reflection, they are also viewed by students as investments in professional careers. This paper draws on a study of 57 second-year students at a research-intensive university in Canada to explore the subjective dimensions of time and school-work rhythms in students' everyday lives. Data suggest that most students expect to work hard, now and in the future, although their backgrounds influence perceptions of the kind of hard work required, and the magnitude and certainty of returns. Students are future-oriented and participation in term-time work is seen as a way of training for future work lives. This training involves adapting bodies to the temporal logics and rhythms of university studies and workplaces. The interplay of rhythms is experienced by some students as harmonious or 'eurhythmic', and by others as discordant or 'arrhythmic'. The extent of discord is related to differences in students' work and studies, differences in their time horizons and value calculations, and differences in family background and resources. This paper contends that understanding students' sense-making in regard to chrono-logics and work-school rhythms is important for building a vision for higher education that better supports human flourishing. [ABSTRACT FROM AUTHOR]

We develop an algorithm for the motion and task planning of a system composed of multiple robots and unactuated objects under tasks expressed as Linear Temporal Logic (LTL) constraints. The robots and objects evolve subject to uncertain dynamics in an obstacle-cluttered environment. The key part of the proposed solution is the intelligent construction of a coupled transition system that encodes the motion and tasks of the robots and the objects. We achieve such a construction by designing appropriate adaptive control protocols in the lower level, which guarantee the safe robot navigation/object transportation in the environment while compensating for the dynamic uncertainties. The transition system is efficiently interfaced with the temporal logic specification via a sampling-based algorithm to output a discrete path as a sequence of synchronized actions of the robots; such actions satisfy the robots' as well as the objects' specifications. The robots execute this discrete path by using the derived low level control protocol. Numerical experiments verify the proposed framework. • Robot tasks expressed by temporal logics offer great versatility and efficiency. • Simple items/objects often have to undergo processes and tasks. • New algorithm provides robot actions that satisfy theirs and objects' tasks. • Robot actions consist of robot navigation and cooperative object transportation. • Adaptive control is used to tackle uncertainty in robots' and objects' dynamics. [ABSTRACT FROM AUTHOR]

We explore the reinforcement learning approach to designing controllers by extensively discussing the case of a quadcopter attitude controller. We provide all details allowing to reproduce our approach, starting with a model of the dynamics of a crazyflie 2.0 under various nominal and non-nominal conditions, including partial motor failures and wind gusts. We develop a robust form of a signal temporal logic to quantitatively evaluate the vehicle's behavior and measure the performance of controllers. The paper thoroughly describes the choices in training algorithms, neural net architecture, hyperparameters, observation space in view of the different performance metrics we have introduced. We discuss the robustness of the obtained controllers, both to partial loss of power for one rotor and to wind gusts and finish by drawing conclusions on practical controller design by reinforcement learning. [ABSTRACT FROM AUTHOR]

Textual descriptions of processes are ubiquitous in organizations, so that documentation of the important processes can be accessible to anyone involved. Unfortunately, the value of this rich data source is hampered by the challenge of analyzing unstructured information. In this paper we propose a framework to overcome the current limitations on dealing with textual descriptions of processes. This framework considers extraction and analysis and connects to process mining via simulation. The framework is grounded in the notion of annotated textual descriptions of processes, which represents a middle-ground between formalization and accessibility, and which accounts for different modeling styles, ranging from purely imperative to purely declarative. The contributions of this paper are implemented in several tools, and case studies are highlighted. [ABSTRACT FROM AUTHOR]

Online monitoring is essential to enhance the reliability for various systems including cyber-physical systems and Web services. During online monitoring, the system traces are checked against monitoring rules in real time to detect deviations from normal behaviors. In general, the rules are defined as boundary conditions by the experts of the monitored system. This work studies the problem of synthesizing online monitoring rules in the form of temporal logic formulas in an automated way. The monitoring rules are described as past-time signal temporal logic (ptSTL) formulas and an algorithm to synthesize such formulas from a given set of labeled system traces is proposed. The algorithm searches the formula space using genetic algorithms and produces the best formula representing a monitoring rule. In addition, online STL monitoring algorithm is improved to efficiently compute a quantitative valuation for piecewise-constant signals from ptSTL formulas, thus, to reduce the overhead of the real-time computation. The effectiveness of the results is shown on two illustrative examples inspired from online monitoring of Web services. [ABSTRACT FROM AUTHOR]

We study an extension of temporal logic, a multi-agent logic on models with nontransitive linear time (which is, in a sense, also an extension of interval logic). The proposed relational models admit lacunas in admissibility relations among agents: information accessible for one agent may be inaccessible for others. A logical language uses temporary operators 'until' and 'next' (for each of the agents), via which we can introduce modal operations 'possible' and 'necessary.' The main problem under study for the logic introduced is the recognition problem for admissibility of inference rules. Previously, this problem was dealt with for a logic in which transitivity intervals have a fixed uniform length. Here the uniformity of length is not assumed, and the logic is extended by individual temporal operators for different agents. An algorithm is found which decides the admissibility problem in a given logic, i.e., it recognizes admissible inference rules. [ABSTRACT FROM AUTHOR]

Reinforcement Learning (RL) is a widely employed machine learning architecture that has been applied to a variety of control problems. However, applications in safety-critical domains require a systematic and formal approach to specifying requirements as tasks or goals. We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs). The given LTL property is translated into a Limit-Deterministic Generalised Büchi Automaton (LDGBA), which is then used to shape a synchronous reward function on-the-fly. Under certain assumptions, the algorithm is guaranteed to synthesise a control policy whose traces satisfy the LTL specification with maximal probability. [ABSTRACT FROM AUTHOR]

Abstract We revisit decidability results for resource-bounded logics and use decision problems on vector addition systems with states (VASS) in order to establish complexity characterisations of (decidable) model checking problems. We show that the model checking problem for the logic RB±ATL is 2 exptime -complete by using recent results on alternating VASS (and in exptime when the number of resources is bounded). Moreover, we establish that the model checking problem for RBTL is expspace -complete. The problem is decidable and of the same complexity for RBTL⁎, proving a new decidability result as a by-product of the approach. When the number of resources is bounded, the problem is in pspace. We also establish that the model checking problem for RB±ATL⁎, the extension of RB±ATL with arbitrary path formulae, is decidable by a reduction to parity games for single-sided VASS (a variant of alternating VASS). Furthermore, we are able to synthesise values for resource parameters. Hence, the paper establishes formal correspondences between model checking problems for resource-bounded logics advocated in the AI literature and decision problems on alternating VASS, paving the way for more applications and cross-fertilizations. [ABSTRACT FROM AUTHOR]

This paper proposes a novel approach to modeling and verifying real-time systems for high reliability. To do so, we first extend projection temporal logic to timed projection temporal logic. Further, we define a timed modeling, simulation, and verification language (TMSVL) for real-time systems. As a result, both systems and desired properties can be expressed in TMSVL. In particular, real-time behaviors such as delay, timeout, and interrupt can be formalized. Compared with commonly used property specification language, TMSVL is capable of specifying more sophisticated properties such as quantitative timing properties, interval-related properties, and periodically repeated properties. Moreover, the unified model checking approach to verifying real-time systems via dynamical program execution is implemented. In addition, a case study for modeling and verifying a $\mu$ C/OS-III multitask system with interrupt is conducted to demonstrate how the proposed approach works. [ABSTRACT FROM AUTHOR]

In previous work, we developed Modal Interface Automata (MIA), an interface theory combining the input/output behaviour of de Alfaro and Henzinger's Interface Automata with the modalities of Larsen's Modal Transition Systems and featuring a conjunction on MIAs. In this paper, we add a temporal logics to MIA based on De Nicola's ACTL. We show how to translate the logical operators to operators on MIAs such that a MIA satisfies a temporal formula if and only if it refines the translation of the formula. This way, MIAs allow heterogeneous specifications with a variety of operational and logical connectives. [ABSTRACT FROM AUTHOR]

Recently, we have shown that satisfiability for the temporal logic E C T L with local constraints over (ℤ, <, =) is decidable using a new technique (Carapelle et al., 2013). This approach reduces the satisfiability problem of E C T L with constraints over some structure $\mathcal {A}$ (or class of structures) to the problem whether $\mathcal {A}$ has a certain model theoretic property that we called EHD (for 'existence of homomorphisms is definable'). Here we apply this approach to structures that are tree-like and obtain several results. We show that satisfiability of E C T L with constraints is decidable over (i) semi-linear orders (i.e., tree-like structures where branches form arbitrary linear orders), (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching trees of height h for each fixed $h\in \mathbb {N}$ . We prove that all these classes of structures have the property EHD. In contrast, we introduce Ehrenfeucht-Fraïssé-games for W M S O + B (weak M S O with the bounding quantifier) and use them to show that the infinite (order) tree does not have the EHD-property. As a consequence, our technique cannot be used to establish whether satisfiability of E C T L with constraints over the infinite (order) tree is decidable. A preliminary version of this paper has appeared as (Carapelle et al., 2015). [ABSTRACT FROM AUTHOR]

We study the linear-time model checking problem for boolean concurrent programs with recursive procedure calls. While sequential recursive programs are usually modeled as pushdown automata, concurrent recursive programs involve several processes and can be naturally abstracted as pushdown automata with multiple stacks. Their behavior can be understood as words with multiple nesting relations, each relation connecting a procedure call with its corresponding return. To reason about multiply nested words, we consider the class of all temporal logics as defined in the book by Gabbay, Hodkinson, and Reynolds (18). The unifying feature of these temporal logics is that their modalities are defined in monadic second-order (MSO) logic. In particular, this captures numerous temporal logics over concurrent and/or recursive programs that have been defined so far. Since the general model checking problem is undecidable, we restrict attention to phase bounded executions as proposed by La Torre, Madhusudan, and Parlato (LICS 24). While the MSO model checking problem in this case is non-elementary, our main result states that the model checking (and satisfiability) problem for all MSO-definable temporal logics is decidable in elementary time. More precisely, it is solvable in time exponential in the formula and ( n+2)-fold exponential in the number of phases where n is the maximal level of the MSO modalities in the monadic quantifier alternation hierarchy (which is a vast improvement over the conference version of this paper from LICS 2013 where the space was also ( n+2)-fold exponential in the size of the temporal formula). We complement this result and provide, for each level n, a temporal logic whose model checking problem is n-EXPSPACE-hard. [ABSTRACT FROM AUTHOR]

Spatial aspects of computation are becoming increasingly relevant when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of system models; however, properties of space are typically not taken into account explicitly. In this position paper we briefly review some of the recent developments of spatial and spatio-temporal model-checking in the context of the European research project QUANTICOL funded by the FET-Proactive programme on Fundamentals of Collective Adaptive Systems. We illustrate some typical applications of spatial and spatio-temporal model checking on collective adaptive systems and provide an outline for further developments. [ABSTRACT FROM AUTHOR]

Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. Grumberg, Kupferman and Sheinvald initiated the research on this topic recently and obtained several interesting results. However, there is still a lack of systematic investigation on the theoretical aspects of the variable extensions of temporal logics. Our goal in this paper is to fill this gap. Around this goal, we make the following choices: 1. We consider the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), and allow arbitrary nestings of variable quantifications with Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL). 2. We investigate the decidability and complexity of both the satisfiability and model checking problems, over both finite and infinite words (trees). In particular, we obtain the following results: Existential variable quantifiers or one single universal quantifier in the beginning already entail the undecidability of the satisfiability problems of both VLTL and VCTL, over both finite and infinite words (trees); if only existential path quantifiers are used in VCTL, then the satisfiability problem (over finite trees) is decidable, no matter which variable quantifiers are available; for VLTL formulae with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variables, then its satisfiability problem becomes decidable, over both finite and infinite words; based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem. [ABSTRACT FROM AUTHOR]

We study the extension of the alternating-time temporal logic ( ATL ) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies. We show that our extension ATL s c is very expressive, but that its decision problems are quite hard: model checking is k - EXPTIME -complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies. [ABSTRACT FROM AUTHOR]

As robots are being integrated into our daily lives, it becomes necessary to provide guarantees on their safe and provably correct operation. Such guarantees can be provided using automata theoretic task and mission planning where the requirements are expressed as temporal logic specifications. However, in real-life scenarios, it is to be expected that not all user task requirements can be realized by the robot. In such cases, the robot must provide feedback to the user on why it cannot accomplish a given task. Moreover, the robot should indicate what tasks it can accomplish which are as “close” as possible to the initial user intent. This paper establishes that the latter problem, which is referred to as the minimal specification revision problem, is NP-complete. A heuristic algorithm is presented that can compute good approximations to the Minimal Revision Problem (MRP) in polynomial time. The experimental study of the algorithm demonstrates that in most problem instances the heuristic algorithm actually returns the optimal solution. Finally, some cases where the algorithm does not return the optimal solution are presented. [ABSTRACT FROM AUTHOR]

Dwyer et al. provide a language to specify dynamic properties based on a limited number of predefined patterns and scopes. The semantics of these properties is defined by translating each combination of a pattern and a scope into usual temporal logics (linear temporal logic, CTL, etc.). This translational semantics suffers from two main issues. It is not easily extensible to other patterns or scopes, and it is not always faithful to the natural semantics. In this article, we propose a compositional automata-based approach defining the semantics of each pattern and each scope by an automaton, after which the semantics is composed. Hence, the semantics is compositional and the language is easily extensible. We compare the two semantics by model checking. In some cases, our semantics reveals a lack of homogeneity within Dwyer et al.'s semantics. Finally, we apply this approach in the context of property-based testing, in order to evaluate the quality of a test suite, by measuring the coverage of the property automaton. To allow the tester to adapt the coverage criteria to its goals, we propose transformation rules over the patterns automata that implement relevant unfolding strategies for loops, or predicates labeling the automata transitions. We illustrate these principles by means of an industrial case study. [ABSTRACT FROM AUTHOR]

Although there have been many works on bounded semantics, a characterization of a good definition for a bounded semantics has not been given, and this has led to definitions of bounded semantics of temporal logics that may not be appropriate with respect to the potential usefulness as a basis for developing bounded model checking approaches. On the other side, the research effort on bounded semantics has mainly focused on existentially interpreted fragments of temporal logics, due to the intricacy of defining appropriate bounded semantics for universally interpreted fragments, or for temporal logics with path quantifiers that are closed under negation. This work addresses these two problems, by defining the characteristics of bounded semantics for clarifying the concept of bounded semantics, and presenting a bounded semantics for the full set of CTL, a logic closed under negation, including possibility for specifying both existential and universal properties. [ABSTRACT FROM AUTHOR]

The outbreak of the COVID-19 pandemic brought renewed attention to electronic voting—this time as a potential option to contain the spread during elections. One of the long unresolved topics with remote voting is the risk of voter's coercion due to the uncontrolled environment in which it takes place, indicating the importance of the coercion resistance property. In the present article, the authors conduct a database analysis of over 350 articles to present different formal definitions of coercion resistance based on three frameworks (game-based definitions, applied pi-calculus, and logic). Finally, the different security properties of each one are studied and compared in order to facilitate the development of electronic voting schemes. [ABSTRACT FROM AUTHOR]

Abstract: In automated synthesis, given a specification, we automatically create a system that is guaranteed to satisfy the specification. In the classical temporal synthesis algorithms, one usually creates a “flat” system “from scratch”. However, real-life software and hardware systems are usually created using preexisting libraries of reusable components, and are not “flat” since repeated sub-systems are described only once. In this work we describe an algorithm for the synthesis of a hierarchical system from a library of hierarchical components, which follows the “bottom-up” approach to system design. Our algorithm works by synthesizing in many rounds, when at each round the system designer provides the specification of the currently desired module, which is then automatically synthesized using the initial library and the previously constructed modules. To ensure that the synthesized module actually takes advantage of the available high-level modules, we guide the algorithm by enforcing certain modularity criteria. We show that the synthesis of a hierarchical system from a library of hierarchical components is Exptime-complete for μ-calculus, and 2Exptime-complete for Ltl, both in the cases of complete and incomplete information. Thus, in all cases, it is not harder than the classical synthesis problem (of synthesizing flat systems “from scratch”), even though the synthesized hierarchical system may be exponentially smaller than a flat one. [Copyright &y& Elsevier]

Abstract: 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. [Copyright &y& Elsevier]

In this paper, we show how to exploit the structure of some automata-based construction to efficiently solve the LTL synthesis problem. We focus on a construction proposed in Schewe and Finkbeiner that reduces the synthesis problem to a safety game, which can then be solved by computing the solution of the classical fixpoint equation ν X. Safe ∩ CPre ( X), where CPre ( X) are the controllable predecessors of X. We have shown in previous works that the sets computed during the fixpoint algorithm can be equipped with a partial order that allows one to represent them very compactly, by the antichain of their maximal elements. However the computation of CPre ( X) cannot be done in polynomial time when X is represented by an antichain (unless P = NP). This motivates the use of SAT solvers to compute CPre ( X). Also, we show that the CPre operator can be replaced by a weaker operator CPre crit where the adversary is restricted to play a subset of critical signals. We show that the fixpoints of the two operators coincide, and so, instead of applying iteratively CPre , we can apply iteratively CPre crit. In practice, this leads to important improvements on previous LTL synthesis methods. The reduction to SAT problems and the weakening of the CPre operator into CPre crit and their performance evaluations are new. [ABSTRACT FROM AUTHOR]

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization. [ABSTRACT FROM AUTHOR]

Quantified CTL (QCTL) extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics , where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE -complete in this framework. We propose a new model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies and we compare them with a prototype (based on several QBF solvers) on different examples. [ABSTRACT FROM AUTHOR]

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMITL , a timed extension of HyperLTL. While the satisfiability problem can be solved similarly as for HyperLTL , we show that the model-checking problem for HyperMITL , unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMITL with quantifier alternations is possible under certain semantic restrictions. As an intermediate tool, we give an 'asynchronous' interpretation of Wilke's monadic logic of relative distance (L d ↔) and show that it characterises timed languages recognised by timed automata with silent transitions. [ABSTRACT FROM AUTHOR]

Abstract: A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on the simplicity of the individual robots; the fault tolerance inherent in having a large population of identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms present an attractive solution to demanding real-world applications, designing individual control algorithms that can guarantee the required global behaviour is a difficult problem. In this paper we assess and apply the use of formal verification techniques for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse whether all possible behaviours within the robot swarm conform to some required specification. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether temporal properties are satisfied on all the possible behaviours of the system. We target a particular swarm control algorithm that has been tested in real robotic swarms, and show how automated temporal analysis can help to refine and analyse such an algorithm. [Copyright &y& Elsevier]

Abstract: Rewriting logic is a simple computational logic that can naturally express both concurrent computation and logical deduction with great generality. This paper provides a gentle, intuitive introduction to its main ideas, as well as a survey of the work that many researchers have carried out over the last twenty years in advancing: (i) its foundations; (ii) its semantic framework and logical framework uses; (iii) its language implementations and its formal tools; and (iv) its many applications to automated deduction, software and hardware specification and verification, security, real-time and cyber-physical systems, probabilistic systems, bioinformatics and chemical systems. [Copyright &y& Elsevier]

Abstract: This bibliography compiles, to the best of our knowledge, all the papers on rewriting logic and its applications which have been written during the more than 20 years that have passed since the introduction of rewriting logic in 1990. The papers are classified according to five main areas: foundations, logical and semantic framework, languages, tools, and applications. [Copyright &y& Elsevier]

Abstract: We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics. [Copyright &y& Elsevier]

Abstract: Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. Recently, a modest extension for LTL by an operator that expresses snapshots, has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one. Originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. In this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. Our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution. [Copyright &y& Elsevier]

Abstract: We consider a class of infinite-state Markov decision processes generated by stateless pushdown automata. This class corresponds to -player games over graphs generated by BPA systems or (equivalently) 1-exit recursive state machines. An extended reachability objective is specified by two sets S and T of safe and terminal stack configurations, where the membership to S and T depends just on the top-of-the-stack symbol. The question is whether there is a suitable strategy such that the probability of hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given . We show that the qualitative extended reachability problem is decidable in polynomial time, and that the set of all configurations for which there is a winning strategy is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This result is a generalization of a recent theorem by Etessami and Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our -player BPA games) is decidable in polynomial time. Interestingly, the properties of winning strategies for the extended reachability objectives are quite different from the ones for termination, and new observations are needed to obtain the result. As an application, we derive the EXPTIME-completeness of the model-checking problem for -player BPA games and qualitative PCTL formulae. [Copyright &y& Elsevier]

Choices in business processes are often based on the process history saved as a log-file listing events and their time stamps. In this paper we introduce LogLogics, a finite-path variant of the Timed Propositional Temporal Logic with Past, which can be in particular used for specifying guards in business process models. The novelty is due to the presence of boundary points corresponding to the starting and current observation points, which gives rise to a three-valued logic allowing us to distinguish between temporal formulas that hold for any log extended with some possible past and future (true), those that do not hold for any extended log (false) and those that hold for some but not all extended logs (unknown). We reduce the check of the truth value of a LogLogics formula to a check on a finite abstraction and present an evaluation algorithm. We also define LogLogics patterns for commonly occurring properties. [Copyright &y& Elsevier]

Abstract: The paper settles a long standing problem for Mazurkiewicz traces: the pure future local temporal logic defined with the basic modalities exists-next and until is expressively complete. This means every first-order definable language of Mazurkiewicz traces can be defined in a pure future local temporal logic. The analogous result with a global interpretation has been known, but the treatment of a local interpretation turned out to be much more involved. Local logics are interesting because both the satisfiability problem and the model checking problem are solvable in Pspace for these logics whereas they are non-elementary for global logics. Both, the (previously known) global and the (new) local results generalize Kamp’s Theorem for words, because for sequences local and global viewpoints coincide. [Copyright &y& Elsevier]

Abstract: This paper studies the complexity of behavior of multi-agent systems. Behavior properties are formulated using classical temporal logic languages and are checked with respect to the transition system induced by the definition of the multi-agent system. We establish various tight complexity bounds of the behavior properties under natural structural and semantic restrictions on agent programs and actions. [Copyright &y& Elsevier]

Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest – the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problemof model checking properties of a class of the logic on Petri hypernets is shown to be PSPACE-complete. [ABSTRACT FROM AUTHOR]

Abstract: In model checking, the state-explosion problem occurs when one checks a nonflat system, i.e., a system implicitly described as a synchronized product of elementary subsystems. In this paper, we investigate the complexity of a wide variety of model-checking problems for nonflat systems under the light of parameterized complexity, taking the number of synchronized components as a parameter. We provide precise complexity measures (in the parameterized sense) for most of the problems we investigate, and evidence that the results are robust. [Copyright &y& Elsevier]

Abstract: We review some results on global and local temporal logic on Mazurkiewicz traces. Our main contribution is to show how to derive the expressive completeness of global temporal logic with respect to first-order logic [V. Diekert, P. Gastin, LTL is expressively complete for Mazurkiewicz traces, J. Comput. System Sci. 64 (2002) 396–418] from the similar result on local temporal logic [V. Diekert, P. Gastin, Pure future local temporal logics are expressively complete for Mazurkiewicz traces, in: M. Farach-Colton (Ed.), Proc. LATIN’04, Lecture Notes in Computer Science, Vol. 2976, Springer, Berlin, 2004, pp. 232–241, Full version available as Research Report LSV-05-22, Laboratoire Spécification et Vérification, ENS Cachan, France]. [Copyright &y& Elsevier]

Abstract: In this paper we prove theorems on the interpretability of the first-order temporal logics LTL and TL into Fork Algebras. This result is part of a research project on the interpretability of logics in Fork Algebras, and has important applications towards the relational specification of properties of systems within the A r g entum tool. [Copyright &y& Elsevier]

Abstract: Model checking and temporal logics are boolean. The answer to the model checking question does a system satisfy a property?is either true or false, and properties expressed in temporal logics are defined over boolean propositions. While this classic approach is enough to specify and verify boolean temporal properties, it does not allow to reason about quantitative aspects of systems. Some quantitative extensions of temporal logics has been already proposed, especially in the context of probabilistic systems. They allow to answer questions like with which probability does a system satisfy a property? We present a generalization of two well-known temporal logics: CTL and the -calculus. Both extensions are defined over c-semirings, an algebraic structure that captures quantitative aspects like quality of service or soft constraints. Basically, a c-semiring consists of a domain, an additive operation and a multiplicative operation, which satisfy some properties. We present the semantics of the extended logics over transition systems, where a formula is interpreted as a mapping from the set of states to the domain of the c-semiring, and show that the usual connection between CTL and -calculus does not hold in general. In addition, we reason about the complexity of computing the logics and illustrate some applications of our framework, including boolean model checking. [Copyright &y& Elsevier]

Abstract: First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed. [Copyright &y& Elsevier]

Our paper proposes a technique for performing logical analysis over the calculi for communication and mobility, i.e., Ambient Calculus type of calculi. We show how this analysis can be used in the case of biological models in order to obtain significant information for biologists. The technique is based on set theoretical models we developed for ambient processes by using the power of Hypersets Theory. These models are further used as possible worlds in a Kripke structure organized for a propositional branching temporal logic. Providing the temporal logical structure for the accessibility relation between ambient processes, we open the perspective of reusing model checking algorithms developed for temporal logics in analyzing any phenomena that can be described by these calculi. [ABSTRACT FROM AUTHOR]

Abstract: Recently, local logics for Mazurkiewicz traces are of increasing interest. This is mainly due to the fact that the satisfiability problem has the same complexity as in the word case. If we focus on a purely local interpretation of formulae at vertices (or events) of a trace, then the satisfiability problem of linear temporal logics over traces turns out to be PSPACE-complete if the dependence alphabet is not part of the input. But now the difficult problem is to obtain expressive completeness results with respect to first order logic. The main result of the paper shows such an expressive completeness result, if the underlying dependence alphabet is a cograph, i.e., if all traces are series parallel posets. Moreover, we show that this is the best we can expect: If the dependence alphabet is not a cograph, then we cannot express all first order properties in our setting. [Copyright &y& Elsevier]

Current workflow management systems still lack support for dynamic and automatic workflow adaptations. However, this functionality is a major requirement for next–generation workflow systems to provide sufficient flexibility to cope with unexpected failure events. We present the concepts and implementation of AgentWork, a workflow management system supporting automated workflow adaptations in a comprehensive way. A rule-based approach is followed to specify exceptions and necessary workflow adaptations. AgentWork uses temporal estimates to determine which remaining parts of running workflows are affected by an exception and is able to predictively perform suitable adaptations. This helps to ensure that necessary adaptations are performed in time with minimal user interaction which is especially valuable in complex applications such as for medical treatments. [Copyright &y& Elsevier]

The problem of testing whether a finite execution trace of events generated by an executing program violates a linear temporal logic (LTL) formula occurs naturally in runtime analysis of software. Two efficient algorithms for this problem are presented in this paper, both for checking safety formulae of the form “always P”, where P is a past-time LTL formula. The first algorithm is implemented by rewriting, and the second synthesizes efficient code from formulae. Further optimizations of the second algorithm are suggested, reducing space and time consumption. Special operators suitable for writing succinct specifications are discussed and shown to be equivalent to the standard past-time operators. This work is part of NASA’s PathExplorer project, the objective of which is to construct a flexible framework for efficient monitoring and analysis of program executions. [ABSTRACT FROM AUTHOR]

Combining knowledge representation and reasoning formalisms is an important and challenging task. It is important because non-trivial AI applications often comprise different aspects of the world, thus requiring suitable combinations of available formalisms modeling each of these aspects. It is challenging because the computational behavior of the resulting hybrids is often much worse than the behavior of their components.In this paper, we propose a new combination method which is computationally robust in the sense that the combination of decidable formalisms is again decidable, and which, nonetheless, allows non-trivial interactions between the combined components.The new method, called E-connection, is defined in terms of abstract description systems (ADSs), a common generalization of description logics, many logics of time and space, as well as modal and epistemic logics. The basic idea of E-connections is that the interpretation domains of n combined systems are disjoint, and that these domains are connected by means of n-ary ‘link relations’. We define several natural variants of E-connections and study in-depth the transfer of decidability from the component systems to their E-connections. [Copyright &y& Elsevier]

The textual Object Constraint Language (OCL) is primarily intended to specify restrictions over UML class diagrams, in particular class invariants, operation pre-, and postconditions. Based on several improvements in the definition of the language concepts in last years, a proposal for a new version of OCL has recently been published [43]. That document provides an extensive OCL semantic description that constitutes a tight integration into UML. However, OCL still lacks a semantic integration of UML Statecharts, although it can already be used to refer to states in OCL expressions. This article presents an approach that closes this gap and introduces a formal semantics for such integration through a mathematical model. It also presents the definition of a temporal OCL extension by means of a UML Profile based on the metamodel of the latest OCL proposal. Our OCL extension enables modelers to specify behavioral state-oriented real-time constraints. It provides an intuitive understanding and readability at application level since common OCL syntax and concepts are preserved. A well-defined formal semantics is given through the mapping of temporal OCL expressions to temporal logics formulae. [ABSTRACT FROM AUTHOR]

The complexity of multi-agent systems behavior properties is studied. The behavior properties are formulated using classical temporal logic languages and are checked relative to the transition system induced by the multi-agent system definition. We show that there are deterministic or nondeterministic polynomial time check algorithms under some realistic structural and semantic restrictions on agent programs and actions. [Copyright &y& Elsevier]