1
$\begingroup$

I'm currently reading Nancy Lynch book about distributed systems, chapter about IO automaton. And I have following questions related to book exercise 8.13(c).

We are given some automaton A with sig(A) is empty. Traces(P) is the set of sequences over {1,2} in wich every occurance of 1 is immediatly followed by a 2. I need to show that P is neither a safety property nor a liveness property. and show explicitly that P could be expressed as intersections of S and L.

Here is my problem: I can show that P is not safety because it breaks prefix-closed property, e.g. {2,1,2} has no prefix belonging to P (it should be of the form {...,1} which is impossible for P). But I don't know how to deal with L property -- either it is empty or include trace(P) -- trace(P) $\subset$ trace(L). If it is empty then traces(P) is empty because traces(P)= traces(S) $\cap$ traces(L) which is wrong. So I think that traces(P) is subset of traces(L).

Is my conclusion related to traces(L) is right?

How can I explicitly express traces(P)=traces(S) $\cap$ traces(L) for this problem?

Thanks in advance.

Improve this question
$\endgroup$
3
  • $\begingroup$ Is this book relevant to your question? It could be self-contained, otherwise could you give the title of the book? $\endgroup$
    – Evil
    Commented Nov 14, 2017 at 17:25
  • $\begingroup$ "Distributed Algorithms" by Nancy Lynch. It is her single book, I believe. First published 20 years ago. Exercise related to chapter 8, async IO automaton. $\endgroup$
    – Sharov
    Commented Nov 14, 2017 at 18:06
  • $\begingroup$ Anyone to rescue?... $\endgroup$
    – Sharov
    Commented Dec 5, 2017 at 20:37

1 Answer 1

Reset to default
1
$\begingroup$

Let S be the set of all traces in which "11" does not appear (a safety property) and L be the liveness property defined such that if 1 appears then eventually 2 will appear after (in temporal logic: $\square( 1 \rightarrow \lozenge 2)$). Then trace(P)=trace(S)$\cap$trace(L).

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.