Prenex universal first-order safety properties

Besik Dundua; Ioane Kapanadze; Helmut Seidl

doi:10.1016/j.ipl.2024.106488

Prenex universal first-order safety properties

Besik Dundua, Ioane Kapanadze, Helmut Seidl

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Research output: Contribution to journal › Article › peer-review

Abstract

We show that every prenex universal syntactic first-order safety property can be compiled into a universal invariant of a first-order transition system using quantifier-free substitutions only. We apply this insight to prove that every such safety property is decidable for first-order transition systems with stratified guarded updates only.

Original language	English
Article number	106488
Journal	Information Processing Letters
Volume	186
DOIs	https://doi.org/10.1016/j.ipl.2024.106488
State	Published - Aug 2024

Keywords

Automatic theorem proving
Decidability
First-order safety LTL
First-order transition system
Formal methods
Parametric systems
Program correctness

Access to Document

10.1016/j.ipl.2024.106488

Cite this

@article{3c7c83cc1bf94e21b907bb5fb6de4f75,

title = "Prenex universal first-order safety properties",

abstract = "We show that every prenex universal syntactic first-order safety property can be compiled into a universal invariant of a first-order transition system using quantifier-free substitutions only. We apply this insight to prove that every such safety property is decidable for first-order transition systems with stratified guarded updates only.",

keywords = "Automatic theorem proving, Decidability, First-order safety LTL, First-order transition system, Formal methods, Parametric systems, Program correctness",

author = "Besik Dundua and Ioane Kapanadze and Helmut Seidl",

note = "Publisher Copyright: {\textcopyright} 2024 The Authors",

year = "2024",

month = aug,

doi = "10.1016/j.ipl.2024.106488",

language = "English",

volume = "186",

journal = "Information Processing Letters",

issn = "0020-0190",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Prenex universal first-order safety properties

AU - Dundua, Besik

AU - Kapanadze, Ioane

AU - Seidl, Helmut

PY - 2024/8

Y1 - 2024/8

N2 - We show that every prenex universal syntactic first-order safety property can be compiled into a universal invariant of a first-order transition system using quantifier-free substitutions only. We apply this insight to prove that every such safety property is decidable for first-order transition systems with stratified guarded updates only.

AB - We show that every prenex universal syntactic first-order safety property can be compiled into a universal invariant of a first-order transition system using quantifier-free substitutions only. We apply this insight to prove that every such safety property is decidable for first-order transition systems with stratified guarded updates only.

KW - Automatic theorem proving

KW - Decidability

KW - First-order safety LTL

KW - First-order transition system

KW - Formal methods

KW - Parametric systems

KW - Program correctness

UR - http://www.scopus.com/inward/record.url?scp=85186332306&partnerID=8YFLogxK

U2 - 10.1016/j.ipl.2024.106488

DO - 10.1016/j.ipl.2024.106488

M3 - Article

AN - SCOPUS:85186332306

SN - 0020-0190

VL - 186

JO - Information Processing Letters

JF - Information Processing Letters

M1 - 106488

ER -

Prenex universal first-order safety properties

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this