کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10333724 | 689170 | 2016 | 22 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Canonical finite models of Kleene algebra with tests
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Kleene algebra with tests (KAT) was introduced by Kozen as an extension of Kleene algebra (KA). So far, the decidability of equational formulas (p=q) and Horn formulas (â§ipi=qiâp=q) in KAT has been investigated by several authors. Continuing this line of research, the current paper studies the decidability of existentially quantified equational formulas âqâP.(p=q) in KAT, where P is a fixed collection of KAT terms and plays a role as a parameter of this decision problem. To design a systematic strategy of deciding problems of this form, given in this paper is an effective procedure of constructing from each KAT term p a finite KAT model K(p) that will be called the canonical finite model of the KAT term p. Applications of this construction are presented, proving the decidability of âqâP.(p=q) for several non-trivial P.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 4, June 2016, Pages 595-616
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 4, June 2016, Pages 595-616
نویسندگان
Takeo Uramoto,