-
Thanks to [Kam68] and [GPSS80], we know that past-time modalities
do not add expressive power to LTL. In [LMS02], we proved that,
in some cases, they may add conciseness: There exist formulas
involving past-time modalities whose translations in LTL are at
least exponentially larger.
On the other hand, the only effective translation of LTL+Past
into LTL is non-elementary. A sketch of a 3-exponential
translation is given in [Mar03].
What is the precise conciseness of past-time modalities
in LTL?
References
| [Kam68] |
Hans W. Kamp.
Tense Logic and the Theory of Linear Order.
PhD thesis. UCLA, Los Angeles, California, USA, 1968.
|
| [GPSS80] |
Dov M. Gabbay, Amir Pnueli, Saharon
Shelah and
Jonathan Stavi.
On the Temporal Analysis of Fairness.
In Conference Record of the 7th ACM Symposium on
Principles of Programming Languages (POPL'80), Las Vegas,
Nevada, USA,
pages 163-173. ACM, 1980.
|
| [LMS02] |
François Laroussinie,
Nicolas Markey and Philippe Schnoebelen.
Temporal Logic with Forgettable Past.
In Proceedings of the 17th Annual Symposium on
Logic in Computer Science (LICS 2002), Copenhagen, Denmark,
pages 383-392. IEEE Comp. Soc. Press, 2002.
|
| [Mar03] |
Nicolas Markey.
Logiques temporelles pour la vérification :
expressivité, complexité, algorithmes.
PhD thesis. Université d'Orléans, France, 2003.
|
-
Along a single, ultimately periodic path, model checking LTL can
be achieved in polynomial time, since a standard labeling
algorithm "à la CTL" can be applied.
On the other hand, the best lower bound we have for that problem
is NC1-hard, since evaluating a boolean function given
a valuation of its variable is NC1-complete.
What is the precise complexity of that problem?
References
| [MS03] |
Nicolas Markey and Philippe Schnoebelen.
Model Checking a Path (Preliminary Report).
In Proceedings of the 14th International Conference on Concurrency
Theory (CONCUR'03), Marseilles, France,
Lecture Notes in Computer Science 2761, pages 251-265. Springer-Verlag, 2003.
|
| [BCGR92] |
Samuel R. Buss, Stephen A. Cook, Arvind Gupta and Vijaya Ramachandran.
An Optimal Parallel Algorithm for Formula Evaluation.
SIAM Journal on Computing 21:755-780, 2002.
|
-
It is well-known that using the region graph construction, reachability can be achieved
in PSPACE in the general framework of Timed Automata, and is even PSPACE-complete [AD94].
In [LMS04], we proved that it is only NLOGSPACE-complete for 1-clock Timed Automata.
As regards 2-clock Timed Automata, we only have an NP-hardness result.
What is the precise complexity of that problem?
References
| [AD94] |
Rajeev Alur and David L. Dill.
A Theory of Timed Automata.
Journal of Theoretical Computer Science, 126(2):183-235, 1994.
|
| [LMS04] |
François Laroussinie,
Nicolas Markey and Philippe Schnoebelen.
Model Checking Timed Automata with One or Two Clocks.
In Proceedings of the 15th International Conference on Concurrency
Theory (CONCUR'04), London, UK,
Lecture Notes in Computer Science 3170, pages 387-401. Springer-Verlag, 2004.
|
-
Given a priced graph G (or, equivalently, a Timed Kripke Structure [LMS02]),
one of its state s, and an positive integer d,
we want to decide whether, along any path in G starting from the state s,
the accumulated cost will eventually be exactly d. This is equivalent to checking that
the CTL formula AF=d TRUE holds in state s.
This problem is obviously in co-NP (a polynomial counter-example being the Parikh image of
a path not satisfying the formula).
Is there a polynomial-time algorithm for that problem?
References
| [LMS02] |
François Laroussinie,
Nicolas Markey and Philippe Schnoebelen.
On Model Checking Durational Kripke structures (Extended Abstract).
In Proceedings of the 5th International Conference on
Foundations of Software Science and Computation Structures (FOSSACS 2002),
Grenoble, France, Lecture Notes in Computer Science 2303,
pages 264-279. Springer-Verlag, 2002.
|
-
Freeze quantifiers are assumed to strictly add expressive
power to (both branching and linear) timed temporal logics. [AH93] gives
the example of a formula
φ = G[ p ⇒ x. F(q ∧ F(r ∧ x ≤ 1)) ]
for which they claim there would be no equivalent MTL formula (assuming
the time domain is a dense linear order). AFAIK, this result has never
been proved.
Can φ be expressed in MTL?
References
| [AH93] |
Rajeev Alur and Thomas A.
Henzinger. Real-time Logics: Complexity and Expressiveness.
Information and Comutation 104(1):35-77. 1993.
|
| [BCM05] |
Patricia Bouyer, Fabrice Chevalier and
Nicolas Markey. On the Expressiveness of TPTL and MTL.
In Proceedings of the 25th Conference on Foundations of Software Technology and
Theoretical Computer Science (FST&TCS'05), Lecture Notes in Computer
Science 3821, pages 432-443. Springer.
|
-
We extend concurrent game structures (CGSs) [AHK02] with (nonnegative) costs
on transitions: those costs indicate the price we have to pay for
firing the corresponding transition. We also extend the logic ATL with
cost constraints on modalities. When costs are positive and
modality constraints are of the form "<c" or ">c", the model-checking
problem remains PTIME [LMO06].
When zero costs are allowed on the transitions of the priced CGS,
the same algorithm fails for modality Until>c. We
are currently only able to prove that the problem is in NP and in coNP.
Is there a polynomial-time algorithm for that problem?
References
| [AHK02] |
Rajeev Alur, Thomas A.
Henzinger, and Orna Kupferman. Alternating-Time Temporal Logic.
Journal of the ACM 49(5):672-713. 2002.
|
| [LMO06] |
François Laroussinie,
Nicolas Markey, and Ghassan Oreiby.
Model Checking Timed ATL for Durational Concurrent Game Structure.
In Proceedings of the 4th International Conference on Formal
Modelling and Analysis of Timed Systems (FORMATS'06), Lecture Notes in Computer
Science 4202, pages 245-259. Springer.
|
|