6533b7d5fe1ef96bd1263b99

RESEARCH PRODUCT

Deciding properties of integral relational automata

Karlis Cerans

subject

Model checkingDiscrete mathematicsClass (set theory)TheoryofComputation_COMPUTATIONBYABSTRACTDEVICESComputer scienceComputer Science::Software EngineeringDecidabilityUndecidable problemComputer Science::Multiagent SystemsCTL*TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESRelational calculusTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSComputer Science::Logic in Computer ScienceAutomata theoryTime complexityComputer Science::Formal Languages and Automata Theory

description

This paper investigates automated model checking possibilities for CTL* formulae over infinite transition systems represented by relational automata (RA). The general model checking problem for CTL* formulae over RA is shown undecidable, the undecidability being observed already on the class of Restricted CTL formulae. The decidability result, however, is obtained for another substantial subset of the logic, called A-CTL*+, which includes all ”linear time” formulae.

yearjournalcountryeditionlanguage
1994-01-01
https://doi.org/10.1007/3-540-58201-0_56