کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6873856 | 1440708 | 2018 | 20 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
First-order μ-calculus over generic transition systems and applications to the situation calculus
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: First-order μ-calculus over generic transition systems and applications to the situation calculus First-order μ-calculus over generic transition systems and applications to the situation calculus](/preview/png/6873856.png)
چکیده انگلیسی
We consider μL, μLa, and μLp, three variants of the first-order μ-calculus studied in verification of data-aware processes, that differ in the form of quantification on objects across states. Each of these three logics has a distinct notion of bisimulation. We show that the three notions collapse for generic dynamic systems, which include all state-based systems specified using a logical formalism, e.g., the situation calculus. Hence, for such systems, μL, μLa, and μLp have the same expressive power. We also show that, when the dynamic system stores only a bounded number of objects in each state (e.g., for bounded situation calculus action theories), a finite abstraction can be constructed that is faithful for μL (the most general variant), yielding decidability of verification. This contrasts with the undecidability for first-order ltl, and notably implies that first-order ltl cannot be captured by μL.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 259, Part 3, April 2018, Pages 328-347
Journal: Information and Computation - Volume 259, Part 3, April 2018, Pages 328-347
نویسندگان
Diego Calvanese, Giuseppe De Giacomo, Marco Montali, Fabio Patrizi,