Solving Łukasiewicz μ-terms

Kyriakos Kalorkoti

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Łukasiewicz μ-calculus was introduced by Mio and Simpson and is an extension of Łukasiewicz logic, introducing scalar multiplication and least as well as greatest fixed points. A key question is how to evaluate terms of this calculus, i.e., find the values of bound variables occurring in a term. In this paper we provide an algorithm that is single exponential in the size of the term (this takes into account the size of rationals occurring in the term and the interpretation of free variables, the number of operators as well as the number of bound variables). We also show that the solutions are polynomially bounded in the size of the input term and interpretation of free variables. The core technique used is the solution of a set of affine fixed point equations with inequalities as side conditions for which a polynomial time algorithm is given. The techniques introduced here may be of wider interest in model checking and distributive systems.
Original languageEnglish
Pages (from-to)38-49
Number of pages12
JournalTheoretical Computer Science
Volume712
Early online date10 Nov 2017
DOIs
Publication statusPublished - 15 Feb 2018

Keywords / Materials (for Non-textual outputs)

  • fixed points
  • Probabilistic μ-calculus
  • Algorithm for evaluating μ-terms

Fingerprint

Dive into the research topics of 'Solving Łukasiewicz μ-terms'. Together they form a unique fingerprint.

Cite this