A modal logic for non-deterministic disambiguation

Abstract

Disambiguation is investigated through Kripke frames with states given by pairs (-e, -phi) of sequences e = e_1 ... e_n and phi = phi_1 ... phi_n of (possibily ambiguous) expressions e_i adn unambiguous formulas phi_i, where phi_i is (in a precise sense) a disambiguation of e_1, relative to a context in which e_1...e_i-1 occurs to the left  (or past) of e_i, and e_i+1 ... e_n occurs to the right (or future) of e_i. The accessibility relations of the frame are of two kinds: on input e, the state (-e, -phi) may move to a state of the form (-e e, -phi phi); without any input, (-e, -phi) may turn to state (-e, -psi), re-interpreting (as it were) the past input data -e. A multi-modal language is defined that captures bisimulation equivalence between models based on such frames. Decidability and finite model property are, under suitable conditions, established.