top

Hybrid languages and temporal logic

P. Blackburn and M. Tzakova. Hybrid languages and temporal logic. Logic Journal of the IGPL, 7(1):27–54, 1999.

Download: [pdf] 

Abstract:

Hybridization is a method invented by Arthur Prior for extending the expressive power of modal languages. Although developed in interesting ways by Robert Bull, and by the Sofia school (notably, George Gargov, Valentin Goranko, Solomon Passy and Tinko Tinchev), the method remains little known. In our view this has deprived temporal logic of a valuable tool. The aim of the paper is to explain why hybridization is useful in temporal logic. We make two major points, the first technical, the second conceptual. First, we show that hybridization gives rise to well-behaved logics that exhibit an interesting synergy between modal and classical ideas. This synergy, obvious for hybrid languages with full first-order expressive strength, is demonstrated for a weaker local language capable of defining the Until operator; we provide a minimal axiomatization, and show that in a wide range of temporally interesting cases extended completeness results can be obtained automatically. Second, we argue that the idea of sorted atomic symbols which underpins the hybrid enterprise can be developed further. To illustrate this, we discuss the advantages and disadvantages of a simple hybrid language which can quantify over paths.

BibTeX: (download)

@ARTICLE{blackburn99:_hybrid,
  author = {P. Blackburn and M. Tzakova},
  title = {Hybrid languages and temporal logic},
  journal = {Logic Journal of the IGPL},
  year = {1999},
  volume = {7},
  pages = {27--54},
  number = {1},
  abstract = {
	Hybridization is a method invented by Arthur Prior for extending the
	expressive power of modal languages. Although developed in interesting
	ways by Robert Bull, and by the Sofia school (notably, George Gargov,
	Valentin Goranko, Solomon Passy and Tinko Tinchev), the method remains
	little known. In our view this has deprived temporal logic of a valuable
	tool.
	The aim of the paper is to explain why hybridization is useful in
	temporal logic. We make two major points, the first technical, the
	second conceptual. First, we show that hybridization gives rise to
	well-behaved logics that exhibit an interesting synergy between modal
	and classical ideas. This synergy, obvious for hybrid languages with
	full first-order expressive strength, is demonstrated for a weaker
	local language capable of defining the Until operator; we provide
	a minimal axiomatization, and show that in a wide range of temporally
	interesting cases extended completeness results can be obtained automatically.
	Second, we argue that the idea of sorted atomic symbols which underpins
	the hybrid enterprise can be developed further. To illustrate this,
	we discuss the advantages and disadvantages of a simple hybrid language
	which can quantify over paths. }
}

Generated by bib2html.pl (written by Patrick Riley ) on Mon Aug 10, 2009 14:52:33