Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


538 users

0 votes

I've solved these questions but the answers are incorrect. Can anyone guide me on where I am doing wrong?

Q1: [[c SU b] WU a]

A1: G(!a & b & !c); G(!a & b & !c)

Q2: [c SB [a SB b]]

A2: G(a & !b & !c); G(!a & !b & c)

in * TF "Information Systems" by (300 points)
edited by

1 Answer

+1 vote

Please repeat the question of the exercise sheet so that also students of later semesters can understand what we are discussing here. The question is that for a given LTL formula φ, we should construct two LTL formulas φ1 and φ2 that satisfy the following requirements:

  1. φ1 and φ2 are not equivalent
  2. φ1 and φ2 are both satisfiable
  3. φ1->!φ and φ2->!φ are valid

For the given formula φ=[[c SU b] WU a], you suggest φ1=G(!a & b & !c) and φ2=G(!a & b & !c) which does obviously violate the first requirement: The formulas are even syntactically the same, so they are definitely equivalent. 

For the second formula φ=[c SB [a SB b]], you suggest φ1=G(a & !b & !c) and φ2=G(!a & !b & c) which are satisfiable and not equivalent. Also, φ1->!φ is valid, but φ2->!φ is not valid: A counterexample is a single path where always !a&!b&c holds which obiviously satisfies φ2 but also satisfies φ.

by (166k points)
Thanks for the help. I've updated my questions as per your instructions for other students.
Imprint | Privacy Policy