Decidability Of Stit Logics

In this dissertation, we study the decidability of stit logics, which take stit operators as their main operators, other operators including tense operators, the historical necessity operator and knowledge operators etc. The work consists of three main results. The first result states that a class of logics based on an indeter-ministic metric tense logic are decidable. To obtain this result, we apply submodel transformations and a variant of the filtration technique to prove the strong finite frame property. This result can be applied to, among others, logics combining agency, time and knowledge, our language however can only contain X (next) and Y (yesterday) as their tense operators. Our second result considers the decidability of logics containing tense operators U (until) and S (since), the historical necessity operators and cstit operators. We show that two logics, which are determinated by the class of bundled Z-stit frames and the class of full bundled Z-stit frames respectively, are decidable. In this proof, we use quasi-models and interpretations technique, first reduce the satisfiability problem of modal formulas to the existence problem of quasi-models, then apply Rabin Theorem to show that the existence problem of quasi-models is deciable. Last, we study the decidability of logics de-terminated by two classes of astit frames CDZA and CQZA, which are the class of bundled astit frames without busy choose sequences and the class of full bundled astit frames without busy choose sequences respectively. In a simliar way to our second result, we apply quasi-models and interpretations technrique to prove that the logics determinated CDZA and CQZA are decidable. Furthermore, we show that these two classes determinate the same logic.