scholarly journals On Computational Tractability for Rational Verification

2019 ◽  
Author(s):  
Julian Gutierrez ◽  
Muhammad Najib ◽  
Giuseppe Perelli ◽  
Michael Wooldridge
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Multiagent Systems ◽  
Polynomial Time ◽  
Multiagent System ◽  
Reactive Systems ◽  
State System ◽  
Polynomial Space ◽  
Game Theoretic ◽  
Mean Payoff

Rational verification involves checking which temporal logic properties hold of a concurrent and multiagent system, under the assumption that agents in the system choose strategies in game theoretic equilibrium. Rational verification can be understood as a counterpart of model checking for multiagent systems, but while model checking can be done in polynomial time for some temporal logic specification languages such as CTL, and polynomial space with LTL specifications, rational verification is much more intractable: it is 2EXPTIME-complete with LTL specifications, even when using explicit-state system representations.  In this paper we show that the complexity of rational verification can be greatly reduced by restricting specifications to GR(1), a fragment of LTL that can represent most response properties of reactive systems. We also provide improved complexity results for rational verification when considering players' goals given by mean-payoff utility functions -- arguably the most widely used quantitative objective for agents in concurrent and multiagent systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space or even in polynomial time.

scholarly journals Converging from branching to linear metrics on Markov chains

2017 ◽  
Vol 29 (1) ◽  
pp. 3-37 ◽  
Author(s):  
GIORGIO BACCI ◽  
GIOVANNI BACCI ◽  
KIM G. LARSEN ◽  
RADU MARDARE
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Temporal Logic ◽  
Polynomial Time ◽  
Linear Time ◽  
Linear Temporal Logic ◽  
Np Hard ◽  
Branching Time ◽  
Threshold Problem ◽  
Ltl Model Checking

We study two well-known linear-time metrics on Markov chains (MCs), namely, the strong and strutter trace distances. Our interest in these metrics is motivated by their relation to the probabilistic linear temporal logic (LTL)-model checking problem: we prove that they correspond to the maximal differences in the probability of satisfying the same LTL and LTL−X(LTL without next operator) formulas, respectively.The threshold problem for these distances (whether their value exceeds a given threshold) is NP-hard and not known to be decidable. Nevertheless, we provide an approximation schema where each lower and upper approximant is computable in polynomial time in the size of the MC.The upper approximants are bisimilarity-like pseudometrics (hence, branching-time distances) that converge point-wise to the linear-time metrics. This convergence is interesting in itself, because it reveals a non-trivial relation between branching and linear-time metric-based semantics that does not hold in equivalence-based semantics.

A LOGIC BASED APPROACH TO PLANNING FOR SPECIFYING A CLASS OF TEMPORALLY EXTENDED GOALS

2004 ◽  
Vol 13 (03) ◽  
pp. 469-485 ◽  
Author(s):  
RAJDEEP NIYOGI
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Polynomial Time ◽  
Linear Temporal Logic ◽  
The Other ◽  
Logical Framework ◽  
Branching Time ◽  
Optimal Plan ◽  
Other Hand ◽  
Planning Procedure

Planning with temporally extended goals has recently been the focus of much attention to researchers in the planning community. We study a class of planning goals where in addition to a main goal there exist other goals, which we call auxiliary goals, that act as constraints to the main goal. Both these type of goals can, in general, be a temporally extended goal. Linear temporal logic (LTL) is inadequate for specification of the overall goals of this type, although, for some situations, it is capable of expressing them separately. A branching-time temporal logic, like CTL, on the other hand, can be used for specifying these goals. However, we are interested in situations where an auxiliary goal has to be satisfiable within a fixed bound. We show that CTL becomes inadequate for capturing these situations. We bring out an existing logic, called min-max CTL, and show how it can effectively be used for the planning purpose. We give a logical framework for expressing the overall planning goals. We propose a sound and complete planning procedure that incorporates a model checking technology. Doing so, we can answer such planning queries as plan existence at the onset besides producing an optimal plan (if any) in polynomial time.

scholarly journals On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

2021 ◽  
Vol 28 (4) ◽  
pp. 356-371
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Complete Solution ◽  
Reactive Systems ◽  
Expressive Power ◽  
Regular Languages ◽  
Specification Languages ◽  
Temporal Logics ◽  
Emptiness Problem

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

scholarly journals On the Model Checking Problem for Some Extension of CTL*

2020 ◽  
Vol 27 (4) ◽  
pp. 428-441
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Reactive Systems ◽  
Expressive Power ◽  
Binary Relations ◽  
Temporal Logics ◽  
Distinctive Features ◽  
Verification Problem ◽  
Finite State ◽  
Infinite Sequences

Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.

scholarly journals Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy

2018 ◽  
Vol 262 ◽  
pp. 241-264 ◽  
Author(s):  
Laura Bozzelli ◽  
Alberto Molinari ◽  
Angelo Montanari ◽  
Adriano Peron ◽  
Pietro Sala
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Polynomial Time ◽  
Interval Temporal Logic ◽  
Low Levels ◽  
Polynomial Time Hierarchy

scholarly journals Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

2019 ◽  
Author(s):  
Francesco Belardinelli ◽  
Wojciech Jamroga ◽  
Damian Kurpiewski ◽  
Vadim Malvone ◽  
Aniello Murano
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Computational Cost ◽  
Expressive Power ◽  
Game Theoretic ◽  
Strategy Logic ◽  
Tractable Reasoning

In this paper we introduce Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that strictly extends the well-known Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies.  Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. Most importantly, we prove that the model checking problem for SL[SG] is PTIME-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned.

scholarly journals Eigenvalue Based Approach for Global Consensus in Multiagent Systems with Nonlinear Dynamics

2014 ◽  
Vol 2014 ◽  
pp. 1-6
Author(s):  
Wei Qian ◽  
Lei Wang
Keyword(s):  
Nonlinear Dynamics ◽  
Multiagent Systems ◽  
Multiagent System ◽  
Symmetric Matrix ◽  
Algebraic Connectivity ◽  
Communication Graph ◽  
Consensus Protocol ◽  
Global Consensus ◽  
The Common ◽  
Analytical Result

This paper addresses the global consensus of nonlinear multiagent systems with asymmetrically coupled identical agents. By employing a Lyapunov function and graph theory, a sufficient condition is presented for the global exponential consensus of the multiagent system. The analytical result shows that, for a weakly connected communication graph, the algebraic connectivity of a redefined symmetric matrix associated with the directed graph is used to evaluate the global consensus of the multiagent system with nonlinear dynamics under the common linear consensus protocol. The presented condition is quite simple and easily verified, which can be effectively used to design consensus protocols of various weighted and directed communications. A numerical simulation is also given to show the effectiveness of the analytical result.

Sign in / Sign up

Export Citation Format

Share Document