Hybrid Multiagent Systems with Timed Synchronization – Specification and Model Checking

2008 ◽  
pp. 205-220 ◽  
Author(s):  
Ulrich Furbach ◽  
Jan Murray ◽  
Falk Schmidsberger ◽  
Frieder Stolzenburg
Keyword(s):  
Model Checking ◽  
Multiagent Systems

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.

Model Checking Hybrid Multiagent Systems for the RoboCup

2008 ◽  
pp. 262-269 ◽  
Author(s):  
Ulrich Furbach ◽  
Jan Murray ◽  
Falk Schmidsberger ◽  
Frieder Stolzenburg
Keyword(s):  
Model Checking ◽  
Multiagent Systems

scholarly journals Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems

2018 ◽  
Author(s):  
Chen Fu ◽  
Andrea Turrini ◽  
Xiaowei Huang ◽  
Lei Song ◽  
Yuan Feng ◽  
...  
Keyword(s):  
Linear Programming ◽  
Model Checking ◽  
Multiagent Systems ◽  
Epistemic Logic ◽  
Mixed Integer ◽  
Model Checker ◽  
Non Linear Programming ◽  
Smt Solver ◽  
Realistic Assumption ◽  
Novel Algorithm

In this work we study the model checking problem for probabilistic multiagent systems with respect to the probabilistic epistemic logic PETL, which can specify both temporal and epistemic properties. We show that under the realistic assumption of uniform schedulers, i.e., the choice of every agent depends only on its observation history, PETL model checking is undecidable. By restricting the class of schedulers to be memoryless schedulers, we show that the problem becomes decidable. More importantly, we design a novel algorithm which reduces the model checking problem into a mixed integer non-linear programming problem, which can then be solved by using an SMT solver. The algorithm has been implemented in an existing model checker and experiments are conducted on examples from the IPPC competitions.

scholarly journals ProMoca: Probabilistic Modeling and Analysis of Agents in Commitment Protocols

2016 ◽  
Vol 57 ◽  
pp. 465-508 ◽  
Author(s):  
Akın Günay ◽  
Yang Liu ◽  
Jie Zhang
Keyword(s):  
Model Checking ◽  
Multiagent Systems ◽  
Probabilistic Model ◽  
Model Uncertainty ◽  
Formal Language ◽  
Probabilistic Model Checking ◽  
Social Commitment ◽  
Modeling And Analysis ◽  
Essential Properties ◽  
Commitment Protocols

Social commitment protocols regulate interactions of agents in multiagent systems. Several methods have been developed to analyze properties of commitment protocols. However, analysis of an agent's behavior in a commitment protocol, which should take into account the agent's goals and beliefs, has received less attention. In this paper we present ProMoca framework to address this issue. Firstly, we develop an expressive formal language to model agents with respect to their commitments. Our language provides dedicated elements to define commitment protocols, and model agents in terms of their goals, behaviors, and beliefs. Furthermore, our language provides probabilistic and non-deterministic elements to model uncertainty in agents' beliefs. Secondly, we identify two essential properties of an agent with respect to a commitment protocol, namely compliance and goal satisfaction. We formalize these properties using a probabilistic variant of linear temporal logic. Thirdly, we adapt a probabilistic model checking algorithm to automatically analyze compliance and goal satisfaction properties. Finally, we present empirical results about efficiency and scalability of ProMoca.

Sign in / Sign up

Export Citation Format

Share Document