search

albertocasagrande / pyModelChecking

A Python model checking package
Other
58 stars 11 forks source link

Any way to describe `==`, `>=`, `<=`... and other comparator symbols. #11

Closed h-mole closed 3 months ago

h-mole commented 3 months ago

Thanks for this awesome library!

But I have a question that I'd like to automatically generate this LTL:

G(Csi --> !(controlAction == CAi))

However, I have not found any operator in LTL standing for == operator, and nothing else performed like this. How could I deal with such problem? Honestly thanks!

albertocasagrande commented 3 months ago

@hzyrc6011 The LTL operands are either atomic propositions or LTL formulas. Thus, Csi, CAi and controlActions should be atomic propositions. If this is the case, what would the semantics of controlAction == CAi be? Are you wondering whether G(CAi <--> controlAction) holds? Can you provide a small model to clarify this point?

h-mole commented 3 months ago

@hzyrc6011 The LTL operands are either atomic propositions or LTL formulas. Thus, Csi, CAi and controlActions should be atomic propositions. If this is the case, what would the semantics of controlAction == CAi be? Are you wondering whether G(CAi <--> controlAction) holds? Can you provide a small model to clarify this point?

I want to describe a safety requirement on a controller.

The model is meaning that: globally, it is dangerous for the controller to provide controlAction CAi, so the controller should never provide this control action. So, the system should satisfy this LTL: G(Csi --> !(controlAction == CAi))

Finally, to solve this, I think I may consider controlAction == CAi as an atomic proposition Control_Action_CAi. So the created formula is: G(Csi --> !(Control_Action_CAi)). Is there any better solutions for this? Thanks!

albertocasagrande commented 3 months ago

@hzyrc6011 Your proposal is the only one that is supported. I am sorry.