• Home
• About Coq
• Get Coq
• Documentation
• Community

Library PAutomata.Transitions

Library PAutomata.Time

Library PAutomata.TimeSyntax

Library PAutomata.Timebase

Library PAutomata.PAutomata

Library PAutomata.PAuto

Library PAutomata.Properties

Library PAutomata.Coercions

Library PAutomata.AutoL

Library PAutomata.LList

Library PAutomata.Trace

Library PAutomata.ABRdef

Library PAutomata.Evenements

Library PAutomata.ABRgen

Library PAutomata.PGM.Queue

Library PAutomata.PGM.Comp

Library PAutomata.PGM.Var

Library PAutomata.PGM.Map

Library PAutomata.PGM.Vpauto

Library PAutomata.PGM.String

Library PAutomata.PGM.Pgm

Library PAutomata.GAutomata

• • Transition systems associated to a g-automata
  • Synchronisation of two g-automata :
• Quelques definitions et resultats sur la synchronisation des etats

Library PAutomata.AutoLMod

• The AutoL structure is parameterized by a set of var names associated with
• The p-automata associated to a localised automata structure
• Synchronisation of a family of localised automata

Library PAutomata.PAutomataMod

• • Transition systems associated to a p-automata
  • Synchronisation of two p-automata :
• Quelques definitions et resultats sur la synchronisation des etats

Library PAutomata.TransMod

• Modelisation of a labelled transition system
  • Definition of the module structure
  • Expected properties of transition systems
    • (access e1 e2) when e2 is reachable from e1
    • (deadlock e) when there is no more transition from e
    • (deadlock e) when there is an infinite path from e
    • (InvStep P s0) when P is preserved by transitions
    • If P is preserved then it holds on states accessible from s0
  • Another synchronisation
• Strong bisimulation
  • Two definitions, proof of equivalence
    • Definition of R is a bisimulation
    • When R is symmetric it is enough to check one direction
    • Two States are equivalents when a bisimulation exists
    • Properties of StateEquiv
  • Equivalence of the two definitions
    • Direct proof of properties of StBEquiv

Library PAutomata.PAutoMod

Library PAutomata.PGAuto

Library PAutomata.gCSMA_CD.Sender

Library PAutomata.gCSMA_CD.Contexte

Library PAutomata.gCSMA_CD.Bus

Library PAutomata.gCSMA_CD.Block_gCSMA_CD

Library PAutomata.gCSMA_CD.preambule

Library PAutomata.Extract

• webmaster
• xhtml valid
• CSS valid