Computer Science – Logic in Computer Science
Scientific paper
2008-08-29
Computer Science
Logic in Computer Science
To appear in the Proceedings of the 6th IEEE Conference on Software Engineering and Formal Methods (SEFM 2008)
Scientific paper
We develop an incremental-tableau-based decision procedure for the multi-agent epistemic logic MAEL(CD) (aka S5_n (CD)), whose language contains operators of individual knowledge for a finite set Ag of agents, as well as operators of distributed and common knowledge among all agents in Ag. Our tableau procedure works in (deterministic) exponential time, thus establishing an upper bound for MAEL(CD)-satisfiability that matches the (implicit) lower-bound known from earlier results, which implies ExpTime-completeness of MAEL(CD)-satisfiability. Therefore, our procedure provides a complexity-optimal algorithm for checking MAEL(CD)-satisfiability, which, however, in most cases is much more efficient. We prove soundness and completeness of the procedure, and illustrate it with an example.
Goranko Valentin
Shkatov Dmitry
No associations
LandOfFree
Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-544331