The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words

Recently, verification and analysis of data words have gained a lot of interest. Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are two extensions of Linear time temporal logic (LTL). In MTL, the temporal operator are indexed by a constraint interval. TPTL is a more powerf...

Full description

Bibliographic Details
Main Author: Feng, Shiguang
Other Authors: Universität Leipzig, Fakultät für Mathematik und Informatik
Format: Doctoral Thesis
Language:English
Published: Universitätsbibliothek Leipzig 2016
Subjects:
Online Access:http://nbn-resolving.de/urn:nbn:de:bsz:15-qucosa-208823
http://nbn-resolving.de/urn:nbn:de:bsz:15-qucosa-208823
http://www.qucosa.de/fileadmin/data/qucosa/documents/20882/Thesis_Feng.pdf
id ndltd-DRESDEN-oai-qucosa.de-bsz-15-qucosa-208823
record_format oai_dc
spelling ndltd-DRESDEN-oai-qucosa.de-bsz-15-qucosa-2088232016-08-30T03:28:53Z The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words Feng, Shiguang Temporale Logik Erfüllbarkeit Ausdruckskraft Komplexität temporal logic satisfiability expressive power path checking complexity counter machine ddc:500 Recently, verification and analysis of data words have gained a lot of interest. Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are two extensions of Linear time temporal logic (LTL). In MTL, the temporal operator are indexed by a constraint interval. TPTL is a more powerful logic that is equipped with a freeze formalism. It uses register variables, which can be set to the current data value and later these register variables can be compared with the current data value. For monotonic data words, Alur and Henzinger proved that MTL and TPTL are equally expressive and the satisfiability problem is decidable. We study the expressive power, satisfiability problems and path checking problems for MLT and TPTL over all data words. We introduce Ehrenfeucht-Fraisse games for MTL and TPTL. Using the EF-game for MTL, we show that TPTL is strictly more expressive than MTL. Furthermore, we show that the MTL definability problem that whether a TPTL-formula is definable in MTL is not decidable. When restricting the number of register variables, we are able to show that TPTL with two register variables is strictly more expressive than TPTL with one register variable. For the satisfiability problem, we show that for MTL, the unary fragment of MTL and the pure fragment of MTL, SAT is not decidable. We prove the undecidability by reductions from the recurrent state problem and halting problem of two-counter machines. For the positive fragments of MTL and TPTL, we show that a positive formula is satisfiable if and only it is satisfied by a finite data word. Finitary SAT and infinitary SAT coincide for positive MTL and positive TPTL. Both of them are r.e.-complete. For existential TPTL and existential MTL, we show that SAT is NP-complete. We also investigate the complexity of path checking problems for TPTL and MTL over data words. These data words can be either finite or infinite periodic. For periodic words without data values, the complexity of LTL model checking belongs to the class AC^1(LogDCFL). For finite monotonic data words, the same complexity bound has been shown for MTL by Bundala and Ouaknine. We show that path checking for TPTL is PSPACE-complete, and for MTL is P-complete. If the number of register variables allowed is restricted, we obtain path checking for TPTL with only one register variable is P-complete over both infinite and finite data words; for TPTL with two register variables is PSPACE-complete over infinite data words. If the encoding of constraint numbers of the input TPTL-formula is in unary notation, we show that path checking for TPTL with a constant number of variables is P-complete over infinite unary encoded data words. Since the infinite data word produced by a deterministic one-counter machine is periodic, we can transfer all complexity results for the infinite periodic case to model checking over deterministic one-counter machines. Universitätsbibliothek Leipzig Universität Leipzig, Fakultät für Mathematik und Informatik Prof. Dr. Markus Lohrey Prof. Dr. Manfred Droste Prof. Dr. Markus Lohrey Prof. Dr. Manfred Droste Prof. Dr. Martin Lange 2016-08-29 doc-type:doctoralThesis application/pdf http://nbn-resolving.de/urn:nbn:de:bsz:15-qucosa-208823 urn:nbn:de:bsz:15-qucosa-208823 http://www.qucosa.de/fileadmin/data/qucosa/documents/20882/Thesis_Feng.pdf eng
collection NDLTD
language English
format Doctoral Thesis
sources NDLTD
topic Temporale Logik
Erfüllbarkeit
Ausdruckskraft
Komplexität
temporal logic
satisfiability
expressive power
path checking
complexity
counter machine
ddc:500
spellingShingle Temporale Logik
Erfüllbarkeit
Ausdruckskraft
Komplexität
temporal logic
satisfiability
expressive power
path checking
complexity
counter machine
ddc:500
Feng, Shiguang
The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words
description Recently, verification and analysis of data words have gained a lot of interest. Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are two extensions of Linear time temporal logic (LTL). In MTL, the temporal operator are indexed by a constraint interval. TPTL is a more powerful logic that is equipped with a freeze formalism. It uses register variables, which can be set to the current data value and later these register variables can be compared with the current data value. For monotonic data words, Alur and Henzinger proved that MTL and TPTL are equally expressive and the satisfiability problem is decidable. We study the expressive power, satisfiability problems and path checking problems for MLT and TPTL over all data words. We introduce Ehrenfeucht-Fraisse games for MTL and TPTL. Using the EF-game for MTL, we show that TPTL is strictly more expressive than MTL. Furthermore, we show that the MTL definability problem that whether a TPTL-formula is definable in MTL is not decidable. When restricting the number of register variables, we are able to show that TPTL with two register variables is strictly more expressive than TPTL with one register variable. For the satisfiability problem, we show that for MTL, the unary fragment of MTL and the pure fragment of MTL, SAT is not decidable. We prove the undecidability by reductions from the recurrent state problem and halting problem of two-counter machines. For the positive fragments of MTL and TPTL, we show that a positive formula is satisfiable if and only it is satisfied by a finite data word. Finitary SAT and infinitary SAT coincide for positive MTL and positive TPTL. Both of them are r.e.-complete. For existential TPTL and existential MTL, we show that SAT is NP-complete. We also investigate the complexity of path checking problems for TPTL and MTL over data words. These data words can be either finite or infinite periodic. For periodic words without data values, the complexity of LTL model checking belongs to the class AC^1(LogDCFL). For finite monotonic data words, the same complexity bound has been shown for MTL by Bundala and Ouaknine. We show that path checking for TPTL is PSPACE-complete, and for MTL is P-complete. If the number of register variables allowed is restricted, we obtain path checking for TPTL with only one register variable is P-complete over both infinite and finite data words; for TPTL with two register variables is PSPACE-complete over infinite data words. If the encoding of constraint numbers of the input TPTL-formula is in unary notation, we show that path checking for TPTL with a constant number of variables is P-complete over infinite unary encoded data words. Since the infinite data word produced by a deterministic one-counter machine is periodic, we can transfer all complexity results for the infinite periodic case to model checking over deterministic one-counter machines.
author2 Universität Leipzig, Fakultät für Mathematik und Informatik
author_facet Universität Leipzig, Fakultät für Mathematik und Informatik
Feng, Shiguang
author Feng, Shiguang
author_sort Feng, Shiguang
title The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words
title_short The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words
title_full The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words
title_fullStr The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words
title_full_unstemmed The Expressive Power, Satisfiability and Path Checking Problems of MTL and TPTL over Non-Monotonic Data Words
title_sort expressive power, satisfiability and path checking problems of mtl and tptl over non-monotonic data words
publisher Universitätsbibliothek Leipzig
publishDate 2016
url http://nbn-resolving.de/urn:nbn:de:bsz:15-qucosa-208823
http://nbn-resolving.de/urn:nbn:de:bsz:15-qucosa-208823
http://www.qucosa.de/fileadmin/data/qucosa/documents/20882/Thesis_Feng.pdf
work_keys_str_mv AT fengshiguang theexpressivepowersatisfiabilityandpathcheckingproblemsofmtlandtptlovernonmonotonicdatawords
AT fengshiguang expressivepowersatisfiabilityandpathcheckingproblemsofmtlandtptlovernonmonotonicdatawords
_version_ 1718380992033456128