The Satisfiability Problem in Linear Multi-agent Knowledge Logic Based on N

Abstract

In this paper we explore the linear logic of multi-agent knowledge using multivalued models. The logic of the language contains the unary operators $K_{j}$ --- $j$ --- the agent knows, $ULK_{G}$ --- unstable local knowledge, $E_{G}$ --- stable local knowledge in the group, and the binary logical operator $AP_{G}$ - the majority opinion. We will show some examples that demonstrate the diversity of this language and its capabilities. Technically we prove decidability of satisfiability problem in the resulting models for our multi-agent logic, develop verification technique and provide some examples.

Keywords

• modal logic
• temporal logic
• common knowledge
• deciding algorithms
• multiagent logic