相关论文: Strategies, model checking and branching-time prop…

Model checking verifies that a model of a system satisfies a given property, and otherwise produces a counter-example explaining the violation. The verified properties are formally expressed in temporal logics. Some temporal logics, such as…

Computation Tree Logic (CTL) and its extensions CTL* and CTL+ are widely used in automated verification as a basis for common model checking tools. But while they can express many properties of interest like reachability, even simple…

We address the problem of learning temporal properties from the branching-time behavior of systems. Existing research in this field has mostly focused on learning linear temporal properties specified using popular logics, such as Linear…

Hyperproperties extend trace properties to express properties of sets of traces, and they are increasingly popular in specifying various security and performance-related properties in domains such as cyber-physical systems, smart grids, and…

This paper addresses the issue of specifying, simulating, and verifying reactive systems in rewriting logic. It presents an executable semantics for probabilistic, timed, and spatial concurrent constraint programming -- here called…

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency…

Alternating-time temporal logic (ATL) and its extensions, including the alternating-time $\mu$-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of…

We consider the problem of automatically inferring specifications in the branching-time logic, Computation Tree Logic (CTL), from a given system. Designing functional and usable specifications has always been one of the biggest challenges…

The two levels of data and actions on those data provided by the separation between equations and rules in rewriting logic are completed by a third level of strategies to control the application of those actions. This level is implemented…

Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path…

Reasoning about strategic abilities is key to AI systems comprising multiple agents, which provide a unified framework for formalizing various problems in game theory, social choice theory, etc. In this work, we propose a probabilistic…

Since the introduction of Alternating-time Temporal Logic (ATL), many logics have been proposed to reason about different strategic capabilities of the agents of a system. In particular, some logics have been designed to reason about the…

Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset…

We continue the investigation of parameterized extensions of Linear Temporal Logic (LTL) that retain the attractive algorithmic properties of LTL: a polynomial space model checking algorithm and a doubly-exponential time algorithm for…

Standpoint linear temporal logic ($SLTL$) is a recently introduced extension of classical linear temporal logic ($LTL$) with standpoint modalities. Intuitively, these modalities allow to express that, from agent $a$'s standpoint, it is…

Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and rewriting strategies are…

In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a technique to approximate the verification of Alternating-time…

The higher-dimensional modal mu-calculus is an extension of the mu-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property that can be expressed in this logic can be checked in…

In order to deal with the systematic verification with uncertain infromation in possibility theory, Li and Li \cite{li12} introduced model checking of linear-time properties in which the uncertainty is modeled by possibility measures. Xue,…

Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties…