A Modal Logic for Cyclic Repeating

A simplified fragment of PDL, denoted by MLCR—a Modal Logic for Cyclic Repeating—is introduced, in which a cyclic repeating of a program α can be expressed. A completeness theorem for MLCR with respect to the intended standard semantics is given. It is proved that MLCR does not possess the finite model property with respect to its standard models, but nevertheless, it possesses this property with respect to some nonstandard models and consequently is decidable.

Authors

• Dimiter Vakarelov

Keywords

No keywords are indexed for this paper.