Toggle navigation
Caal
Project
New Project
Save
To File
To My Projects
Load
From File
My CCS Projects
My TCCS Projects
CCS Examples
TCCS Examples
Bachelor Thesis Examples
Delete
My CCS Projects
My TCCS Projects
Export
To PDF
To PDF with properties
Edit
Explore
Verify
Games
Equivalence Games
HML Game
Spectroscopy Energy Game
About
Syntax
10
12
14
16
18
20
22
24
CCS
TCCS
Parse
Options
Strong Successors (→)
Weak Successors (⇒)
No Bisimulation Collapse
Strong Bisimulation Collapse
Weak Bisimulation Collapse
Strong Timed Successors (→
t
)
Strong Untimed Successors (→
u
)
Weak Timed Successors (⇒
t
)
Weak Untimed Successors (⇒
u
)
No Bisimulation Collapse
Strong Timed Bisimulation Collapse
Weak Timed Bisimulation Collapse
Strong Untimed Bisimulation Collapse
Weak Untimed Bisimulation Collapse
Apply Structural Reductions
Fullscreen
Source
Action
Target
Add Property
Stop
Verify All
Verify with BJN-Algorithm
Delete all
Status
Time
Property
Verify
Edit
Delete
Options
×
Close
Add/Edit Property
Property Type
Equivalence/Preorder Checking
Model Checking
Left Process
Type
Strong
Weak
Strong Timed
Strong Untimed
Weak Timed
Weak Untimed
Relation
Simulation
Simulation Equivalence
Bisimulation
Trace Inclusion
Trace Equivalence
Two-Nested Simulation
Ready Simulation
Readiness Traces
Possible Futures
Failure Traces
Readiness
Revivals
Impossible Futures
Failures
Enabledness
BJN-Algorithm
Right Process
Process
⊨
Formula
Variable Definition(s)
Comment
Strong
Weak
Strong Timed
Strong Untimed
Weak Timed
Weak Untimed
Simulation
Bisimulation
Attacker
Defender
Restart
Fullscreen
Source
Action
Target
Restart
Fullscreen
Strong
Bisimulation
Two-Nested Simulation
Ready Simulation
Possible Futures
Simulation
Readiness Traces
Failure Traces
Readiness
Impossible Futures
Revivals
Failures
Trace Inclusion
Enabledness
Attacker
Defender
Restart
Energy Budget:
Fullscreen
Source
Update
Target
×
Close
×
Close