A first order logic for specification of timed algorithms: Basic properties and a decidable class

DOI10.1016/S0168-0072(01)00049-5zbMath0988.03055OpenAlexW2051073429MaRDI QIDQ5957904

Danièle Beauquier, Anatol Slissenko

Publication date: 20 May 2002

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(01)00049-5

zbMATH Keywords

verificationfinitenessfirst-order logicdecidabilityspecificationblock Gurevich abstract state machinesgeneralized railroad crossing problemreactive real-time systemsreals with timed functionstimed algorithmstimed logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items

Periodicity based decidable classes in a first order timed logic, Decidable Fragments of Many-Sorted Logic, Decidable properties for monadic abstract state machines, A first order logic for specification of timed algorithms: Basic properties and a decidable class, Decidable fragments of many-sorted logic, Decidable verification for reducible timed automata specified in a first order logic with time, Moded and continuous abstract state machines

Uses Software

• PVS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• A calculus of durations
• A theory of timed automata
• Decidable verification for reducible timed automata specified in a first order logic with time
• Expressive completeness of duration calculus.
• On the decidability of continuous time specification formalisms
• A new solution of Dijkstra's concurrent programming problem
• Evolving Algebras 1993: Lipari Guide
• A first order logic for specification of timed algorithms: Basic properties and a decidable class