A Logic of Sights

We study labeled transition systems where at each state an agent is aware of and hence reasons about only a part of the entire system (called the ‘sight’). We develop a logic for such systems: the ‘logic of sights’. We explore its model theory, give an axiomatization and prove its completeness. We show that the logic is a fragment of the loosely guarded fragment of first-order logic. We show that the satisfiability problem of the logic is PSPACE-complete and the combined complexity of its model-checking problem is in PTIME. Finally we discuss its relation to other logics as well as extensions