marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-05-05 08:47:04

Browse source
This commit is contained in:
Marco Realacci 2025-05-05 08:47:04 +02:00
parent eeeab36055
commit 13fbfd08ec
3 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
Concurrent Systems/notes/15 - A formal language for LTSs.md
View file

@ -16,4 +16,9 @@ The language generated by this grammar will be denoted by Form; every element of
![](../../Pasted%20image%2020250505083948.png)
To simplify the proofs, we consider a more general form of conjunction: $\land_{i \in I, \phi i}$
To simplify the proofs, we consider a more general form of conjunction: $$\land_{i \in I, \phi_{i}}$$
where I is any indexing set (possibility, also infinite). Satisfiability for this operator is similar to that for the binary operator.
Of course, we can use the boolean constant FALSE (FF) and classical logical operators like disjunction $\lor$ and implication $=>$ (they can all be derived in the usual way from $TT, \lnot, \land$).
Another very useful logical operator is "box": let us define $\lnot \lozenge a p$