Hello,

I think I figured it out, just using LTL syntax - "!p2 & X(p1 & p2) & XX(!p1 & !p2) & XXX{p1 & p2}"
Regards,
Phillipp

On Mon, 23 Nov 2020 at 11:14, Philip Schwartz <pschwartz090@gmail.com> wrote:

Thank you very much.

Can I transfer this word to an automata - "!p2; p1 & p2; !p1 & !p2; cycle{p1 & !p2}" using spot translate?

Regards,
Phillipp

On Mon, 23 Nov 2020 at 10:31, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
On Mon, Nov 23, 2020 at 7:55 AM Philip Schwartz <pschwartz090@gmail.com> wrote:
>
> Hello Prof. Alexandre Duret-Lutz
>
> Is it possible to do a straightforward intersection between 2 automatas and check if the intersection has an accepting state?

if aut1.intersects(aut2):
...

--
Alexandre Duret-Lutz