Output details

Linear Temporal Logic LTL_K extended by multi-agent logic K_n with interacting agents

<11>This paper solves an important and difficult open problem. It constructs an algorithm verifying satisfiability for conditions and statements in a temporal linear multi-agent logic with interacting agents. This algorithm works via computing truth values of special formulas in finite models of bounded size. This multi-agent logic is one of most popular ones in the area of Information Sciences and Computer Science. It may find application in multi-agent reasoning, e.g. - decision taking, voting in concurrency. Our algorithm can compute satisfiable and contradictory statements, recognize dependence of specifications and descriptions, and compute and extract common knowledge from collected information.