From Accepting Computation to Satisfying Kripke Model.

Ausema, Chris (2021) From Accepting Computation to Satisfying Kripke Model. Bachelor's Thesis, Computing Science.

Preview	Text bCS_2021_Ausema.pdf.pdf Download (398kB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (125kB)

Abstract

A method that can be used to find the time complexity of a problem is to reduce it to another problem, or vice versa. In the book Dynamic logic by David Harel, Dexter Kozen and Jerzy Tiuryn, it is shown that you can find the lower bound complexity of the satisfiability problem of PDL by using reduction from the membership problem for polynomial space bound single tape alternating Turing machines (PSST ATM). The proof shown was an informal high level proof, which only showed the intuition behind their proof and could therefore benefit from a more rigorous presentation. We will use the definitions of PDL and PSST ATMs to show a more detailed presentation of half their proof. In this thesis we will show that when a PSST ATM has an accepting computation on some input, then a Kripke model exists that encodes the workings of the PSST ATM

Item Type:	Thesis (Bachelor's Thesis)
Supervisor name:	Hansen, H.H. and Ramanayake, D.R.S.
Degree programme:	Computing Science
Thesis type:	Bachelor's Thesis
Language:	English
Date Deposited:	04 Oct 2021 08:35
Last Modified:	04 Oct 2021 08:35
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/26150

Actions (login required)

View Item