A modal logic for non-deterministic disambiguation
A modal logic is presented for Kripke frames with states
(i.e., possible worlds) given by pairs (e-,phi-) of sequences e- = e_1 ... e_n
and phi- = phi_1 ... phi_n of possibly ambiguous expressions e_i and
(unambiguous) formulas phi_i, where phi_i is (in a precise sense) a
disambiguation of e_i 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:
transitions labeled by expressions e, with "(e-,phi-) e-> (e'-,phi'-)" iff
e'- = e-e and phi'- = phi-phi; and unlabeled transitions (e-,phi-) d->
(e'-,phi'-) iff e- = e'-. Transitions of the first type, e->
describe (non-deterministic) extensions of a state
(e-,phi') assuming e occurs to the right/future of e-. Transitions
of the second kind allow for a re-interpretation
phi'- of the first component e- of a state
(e-,phi-). A multi-modal language is defined that captures
bisimulation equivalence between models based on such frames. Decidability and
the finite model property are, under suitable conditions, established.
Tim Fernando