scholarly journals Representation and Reasoning about Strategic Abilities with ω-Regular Properties

Mathematics ◽  
2021 ◽  
Vol 9 (23) ◽  
pp. 3052
Author(s):  
Liping Xiong ◽  
Sumei Guo
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Research Area ◽  
Regular Expressions ◽  
Multi Agent Systems ◽  
Practical Applications ◽  
Multi Agent ◽  
Strategy Logic ◽  
Active Research

Specification and verification of coalitional strategic abilities have been an active research area in multi-agent systems, artificial intelligence, and game theory. Recently, many strategic logics, e.g., Strategy Logic (SL) and alternating-time temporal logic (ATL*), have been proposed based on classical temporal logics, e.g., linear-time temporal logic (LTL) and computational tree logic (CTL*), respectively. However, these logics cannot express general ω-regular properties, the need for which are considered compelling from practical applications, especially in industry. To remedy this problem, in this paper, based on linear dynamic logic (LDL), proposed by Moshe Y. Vardi, we propose LDL-based Strategy Logic (LDL-SL). Interpreted on concurrent game structures, LDL-SL extends SL, which contains existential/universal quantification operators about regular expressions. Here we adopt a branching-time version. This logic can express general ω-regular properties and describe more programmed constraints about individual/group strategies. Then we study three types of fragments (i.e., one-goal, ATL-like, star-free) of LDL-SL. Furthermore, we show that prevalent strategic logics based on LTL/CTL*, such as SL/ATL*, are exactly equivalent with those corresponding star-free strategic logics, where only star-free regular expressions are considered. Moreover, results show that reasoning complexity about the model-checking problems for these new logics, including one-goal and ATL-like fragments, is not harder than those of corresponding SL or ATL*.

scholarly journals A Modal Logic for Joint Abilities under Strategy Commitments

2020 ◽  
Author(s):  
Zhaoshuai Liu ◽  
Liping Xiong ◽  
Yongmei Liu ◽  
Yves Lespérance ◽  
Ronghai Xu ◽  
...  
Keyword(s):  
Modal Logic ◽  
Temporal Logic ◽  
Dynamic Logic ◽  
Research Area ◽  
Multi Agent Systems ◽  
Logical Frameworks ◽  
Dominated Strategies ◽  
Multi Agent ◽  
Active Research ◽  
Active Research Area

Representation and reasoning about strategic abilities has been an active research area in AI and multi-agent systems. Many variations and extensions of alternating-time temporal logic ATL have been proposed. However, most of the logical frameworks ignore the issue of coordination within a coalition, and are unable to specify the internal structure of strategies. In this paper, we propose JAADL, a modal logic for joint abilities under strategy commitments, which is an extension of ATL. Firstly, we introduce an operator of elimination of (strictly) dominated strategies, with which we can represent joint abilities of coalitions. Secondly, our logic is based on linear dynamic logic (LDL), an extension of linear temporal logic (LTL), so that we can use regular expressions to represent commitments to structured strategies. We analyze valid formulas in JAADL, give sufficient/necessary conditions for joint abilities, and show that model checking memoryless JAADL is in EXPTIME.

scholarly journals Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications

2019 ◽  
Author(s):  
Jakub Michaliszyn ◽  
Piotr Witkowski
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Order Logic ◽  
Regular Expressions ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Interval Temporal Logic ◽  
Multi Agent ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Epistemic Halpern-Shoham logic (EHS) is an interval temporal logic defined to verify properties of Multi-Agent Systems. In this paper we show that the model checking Multi-Agent Systems with regular expressions against the EHS specifications is decidable. We achieve this by reducing the model checking problem to the satisfiability problem of Monadic Second-Order Logic on trees.

Realizing the NOSHAPE MAS Organizational Model

2015 ◽  
Vol 7 (2) ◽  
pp. 75-104 ◽  
Author(s):  
Hosny Ahmed Abbas
Keyword(s):  
Large Scale ◽  
Real Life ◽  
Research Area ◽  
Multi Agent Systems ◽  
Organizational Model ◽  
Design Decisions ◽  
Agent Systems ◽  
Multi Agent ◽  
Active Research ◽  
Great Focus

Dynamic reorganization of multi-agent systems (MAS) is currently an interesting and active research area. New emerging concepts such as self-organization and emergence are also getting great focus by MAS research community because of their captivating benefits for engineering complex large-scale MAS applications. Dynamic reorganization is considered as an effective way for building adaptive MAS. This paper provides an operational view of the conceptually proposed NOSHAPE dynamic organizational model for dynamically reorganized multi-agent systems (Abbas, 2014). The operational view concerns possible design decisions, implementation issues, and suggested usage of the NOSHAPE model for practically engineering real life applications. This paper also identifies the possible solutions to be applied throughout the system design to resolve these concerns.

scholarly journals Applications and Challenges of Deep Reinforcement Learning in Multi-robot Path Planning

2021 ◽  
Vol 5 (6) ◽  
pp. 25-29
Author(s):  
Tianyun Qiu ◽  
Yaxuan Cheng
Keyword(s):  
Reinforcement Learning ◽  
Path Planning ◽  
Research Area ◽  
Training Methods ◽  
Multi Agent Systems ◽  
Robot Path Planning ◽  
Practical Applications ◽  
Multi Agent ◽  
Robot Path ◽  
Multi Robot

With the rapid advancement of deep reinforcement learning (DRL) in multi-agent systems, a variety of practical application challenges and solutions in the direction of multi-agent deep reinforcement learning (MADRL) are surfacing. Path planning in a collision-free environment is essential for many robots to do tasks quickly and efficiently, and path planning for multiple robots using deep reinforcement learning is a new research area in the field of robotics and artificial intelligence. In this paper, we sort out the training methods for multi-robot path planning, as well as summarize the practical applications in the field of DRL-based multi-robot path planning based on the methods; finally, we suggest possible research directions for researchers.

scholarly journals Dynamic Linear Time Temporal Logic

1997 ◽  
Vol 4 (8) ◽  
Author(s):  
Jesper G. Henriksen ◽  
P. S. Thiagarajan
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Order Theory ◽  
Simple Extension ◽  
Propositional Dynamic Logic ◽  
First Order ◽  
Time Semantics ◽  
Linear Time Temporal Logic ◽  
Obvious Manner

A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.

Sign in / Sign up

Export Citation Format

Share Document