Some Results in Dynamic Model Theory

Abstract

First-order structures over a fixed signature give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are valuations of program variables and whose atomic actions are state changes elected by variable assignments x := e, where e is a Epsilon term. The Kleene algebras with tests that arise in this way play a role in dynamic model theory akin to the role played by Lindenbaum algebras in classical first-order model theory. Given a first-order theory T over Epsilon, we exhibit a Kripke frame U whose trace algebra TrU is universal for the equational theory of Tarskian trace algebras over Epsilon satisfying T, although U itself is not Tarskian in general. The corresponding relation algebra RelU is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2004
Accession Number
AD1000352

Entities

People

  • Dexter Kozen

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Automata
  • Boolean Algebra
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Electronic Mail
  • Identities
  • Language
  • Logic
  • Model Theory
  • Models
  • New York
  • Programming Languages
  • Sequences
  • Theorems
  • Universities

Fields of Study

  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.