Re: [Concurrency] Temporal logic formula conflict detection
Vaughan’s answer made me realize that you can look at this question from
very different perspectives, so I would like to add mine.
The question of conflict detection in temporal logic is normally asked
in the setting of something like Linear Temporal Logic (LTL). A “model”
is usually one of two things: an infinite trace (of valuations to the
propositional symbols), or a system, i.e., something like a Mealy machine.
If models are traces, the question is known as “satisfiability” and a
good place to start is Manna & Pnueli [0]. A modern contribution to the
detection of such conflicts is given by Cimatti et al in a CAV 2007
paper [1]. For LTL, this question is PSPACE-complete and is considered
relatively easy.
If models are systems, as the original email suggests they should be,
the question is known as “realizability”. This question goes back to
Church (for S1S) [2] and was solved by Buechi and Landweber [3] and
Rabin [4]. In the setting of LTL, it was posed and solved by Pnueli and
Rosner [5]. This question is very hard: for LTL it is 2EXP-complete.
More modern work (which allows you to look up references) is again by
Cimatti [6]. There is also work in this direction by my group; the
introduction of Jobstmann’s thesis will give you a historical
perspective [7].
Best,
Roderick Bloem
[0] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent
Systems *Specification*. Springer-Verlag, 1991.
[1] Alessandro Cimatti, Marco Roveri
,
Viktor Schuppan
,
Stefano Tonetta
:
Boolean Abstraction for Temporal Logic Satisfiability. CAV 2007
:
532-546
[2] A. Church. Logic, arithmetic and automata. In Proceedings International
Mathematical Congress, 1962.
[3] J. R. B?uchi and L. H. Landweber. Solving sequential conditions by
finite-state
strategies. Transactions of the American Mathematical Society, 138:295?311,
1969.
[4] M. O. Rabin. Automata on Infinite Objects and Church?s Problem. Regional
Conference Series in Mathematics. American Mathematical Society, Providence,
RI, 1972.
[5] A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc.
Symposium on Principles of Programming Languages (POPL ?89), pages 179?
190, 1989.
[6] Alessandro Cimatti, Marco Roveri
,
Viktor Schuppan
,
Andrei Tchaltsev
:
Diagnostic Information for Realizability. VMCAI 2008
:
52-67
[7] http://mtc.epfl.ch/~jobstman/bib/files/BJ-PhD_Thesis.pdf,
http://mtc.epfl.ch/~jobstman/bib/index.html
Vaughan Pratt wrote:
> The one-sentence answer would be that temporal logic does not
> distinguish between conflict of A and B in your sense and
> unsatisfiability of A&B, whence any research specifically directed to
> conflict per se would most likely start from some other sense of the
> word “conflict.”
>
> In more detail, for any logical framework that has a semantics and
> includes ordinary conjunction & in its language, such as temporal
> logic but many others of course including intuitionistic, relevant,
> and other variants, formulas A and B are in conflict in your sense
> just when the formula A&B admits no model (almost your original
> question but now with a single formula).
>
> In any logical framework that makes all formulas not admitting a model
> logically equivalent to each other, with FALSE as their canonical
> representative, A and B are in conflict when A&B is false in that sense.
>
> This logical conception of conflict assimilates the concept into the
> larger framework of logic, making its detection a special case of the
> more general problem of determining logical relationships among
> formulas. This is the basis for the one-sentence answer’s conclusion
> that any research specifically on conflict detection in temporal logic
> would be on account of viewing conflict as more than merely
> unsatisfiability.
>
> There are other notions of conflict besides the semantically based one
> you asked about. A proof theoretic notion of conflict would be that A
> and B are in conflict when together they entail C for any formula C.
> In relevant logic this fails to capture conflict as usually understood
> because A and B may be in conflict and yet not even together entail
> the composition of the moon. Hence relevant logic weakens the notion
> of conflict to the requirement that A and B entail FALSE. Since
> relevant logic ordinarily has two notions of FALSE this means that in
> the relevant logic of concurrent behavior there are two notions of
> conflict, the stronger one being that entailing BOTTOM, the sort of
> conflict that can shut down the grid of an entire galaxy and that does
> entail the composition of the moon. (I’m shaky on relevant logic,
> please BE BOLD if you spot an error.)
>
> Standalone models of concurrency that do not rely primarily on logic
> for their expression such as Petri nets, event structures, Chu spaces,
> and so on make more explicit provision of one kind or another for
> expressing conflict. On the one hand this takes us outside the scope
> of your question as phrased, on the other conflict tends to become a
> more interesting concept in its own right when logic is not around to
> obscure its intuitive meaning by assimilating it into its framework,
> where systems like Boolean logic accord equal rights to 0 and 1 with
> the nonchalance of *film noir* and do not consider conflict in any way
> structurally different from vacuity, a distinction that is convenient
> to ignore for some purposes but not others.
>
> Vaughan Pratt
>
> Awad, Ahmed wrote:
>> Hello,
>>
>>
>>
>> I would like to ask if you are aware of some research work regarding
>> conflict detection between properties that are written as temporal
>> logic formula.
>>
>>
>>
>> I need to decide whether formula A and B are in conflict i.e. there
>> does not exist a system that satisfies both of them
>>
>>
>>
>> Regards,
>>
>> Ahmed
_______________________________________________
Concurrency mailing list
Concurrency@listserver.tue.nl
http://listserver.tue.nl/mailman/listinfo/concurrency