Welcome to UPPAAL-Meta Discussions!

[yrke]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[hkr-droid]

Hello,

I'm hkr and I am a PhD student in the computer science department at University of California.  My background is programming language theory/design and I spend a lot of time messing around with the interactive theorem prover Agda. I recently discovered timed automata and found a way to use Uppaal for a project in my lab. Since then I've become very interested in modeling and verifying real time/reactive systems. 

I was hoping to ask a few basic questions about timed automata, specifically equivalence relations defined over them. As you might guess from my attachment to type theory, I'm used to applying equational reasoning or axiom/rewriting to prove things. In applying this approach to timed automata, or really just switching over to an automata-theoretic way of looking at things, I've hit a snag.

If you have any questions, feel free to reach out. Looking forward to talking about reactive systems!