کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
427618 | 686529 | 2013 | 5 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: Satisfiability problem for modal logic with global counting operators coded in binary is NExpTime-complete Satisfiability problem for modal logic with global counting operators coded in binary is NExpTime-complete](/preview/png/427618.png)
This paper provides a proof of NExpTime-completeness of the satisfiability problem for the logic K(En)K(En) (modal logic K with global counting operators), where number constraints are coded in binary. Hitherto the tight complexity bounds (namely ExpTime-completeness) have been established only for this logic with number restrictions coded in unary. The upper bound is established by showing that K(En)K(En) has the exponential-size model property and the lower bound follows from reducibility of exponential bounded tiling problem to K(En)K(En).
► We prove NExpTime-completeness of modal logic with counting operators coded in binary.
► We establish the upper bound by proving the exponential-size model property with a precise bounding function.
► We establish the lower bound by encoding the bounded tiling problem within the logic.
► We draw possible extensions of the complexity proof on the logics defined over various frame classes.
Journal: Information Processing Letters - Volume 113, Issues 1–2, January 2013, Pages 34–38