A higher order modal fixed point logic

Mahesh Viswanathan, Ramesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

We present a higher order modal fixed point logic (HFL) that extends the modal μ-calculus to allow predicates on states (sets of states) to be specified using recursively defined higher order functions on predicates. The logic HFL includes negation as a first-class construct and uses a simple type system to identify the monotonic functions on which the application of fixed point operators is semantically meaningful. The model checking problem for HFL over finite transition systems remains decidable, but its expressiveness is rich. We construct a property of finite transition systems that is not expressible in the Fixed Point Logic with Chop [1] but which can be expressed in HFL. Over infinite transition systems, HFL can express bisimulation and simulation of push down automata, and any recursively enumerable property of a class of transition systems representing the natural numbers.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsPhilippa Gardner, Nobuko Yoshida
PublisherSpringer
Pages512-528
Number of pages17
ISBN (Print)354022940X, 9783540229407
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3170
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A higher order modal fixed point logic'. Together they form a unique fingerprint.

Cite this