Experiment with Gen AI for rule and model generation

[foysavas]

Useful links about LTL:

• https://www.ltl-tutor.xyz/
• https://blog.brownplt.org/2024/08/08/ltltutor.html
• https://cs.brown.edu/~sk/Publications/Papers/Published/gsnk-little-tricky-logic/

LLMs prompts:

write an LTL (linear temporal logic) rules for the following english text:
PartyA and PartyB must agree on changes.
PartyA may add up to $1000 of payables without PartyB's approval.
PartyB may end the agreement at anytime.

Or alternatively ask it for modal mu calculus.

synthesize a kripke structure that satisfies these rules