The Set of Probabilistic Algorithmic Formulas Valid in a Finite Structure Is Decidable with Respect to Its Diagram

Article type: Research Article

Authors: Dańko, Wiktor

Affiliations: Institute of Mathematics, University of Warsaw, Bialystok Division, Akademicka 2, 15-267 Bialystok, Poland

Abstract: In the paper it is considered a probabilistic logic of programs PrAL, similar to the Feldman-Harel logic, constructed for expressing properties of iterative programs with operations x:=?, either … or … interpreted in a probabilistic way. A language of PrAL contains a sort of variables interpreted as real numbers, used to describe probabilities of behaviours of programs. The main result states that the set of formulas of PrAL valid in a finite structure is decidable with respect to the diagram of the structure.

DOI: 10.3233/FI-1993-193-411

Journal: Fundamenta Informaticae, vol. 19, no. 3-4, pp. 417-431, 1993