Anonymous
6/12/2025, 3:37:09 PM
No.105571365
>>105565545
Discrete mathematics might be enough if you're a self starter, and willing to learn as you go.
I'd say Non-Deterministic (LTL, CTL, CTL*) model checking is more mathematical maturity heavy, but light on the actual prerequisites.
Probabilistic model checking is much harder on the actual maths you need to know (you'll need to have a reasonable working grasp of Markov Chains), and if you want to get into the details of how checkers work you'll also need lots of Monte Carlo type stuff, but the topic is generally less abstract.
Ideally for the non-deterministic stuff (the main stuff), you should have a proper formal logic course (dealing logic as a grammar which generates formal sentences, and then semantics being derived Boolean functions on them, by way of assignments) and a "Models of Computation" type automata-theory/language course as LTL checking relies on omega regular languages and Generalised non-deterministic Buchi automata and these are quite a bitch to get your head around if you haven't seen DFAs/NFAs. I only took my Uni's base course in FV but I looked into the second course and there's a lot about working with infinite automata.
Discrete mathematics might be enough if you're a self starter, and willing to learn as you go.
I'd say Non-Deterministic (LTL, CTL, CTL*) model checking is more mathematical maturity heavy, but light on the actual prerequisites.
Probabilistic model checking is much harder on the actual maths you need to know (you'll need to have a reasonable working grasp of Markov Chains), and if you want to get into the details of how checkers work you'll also need lots of Monte Carlo type stuff, but the topic is generally less abstract.
Ideally for the non-deterministic stuff (the main stuff), you should have a proper formal logic course (dealing logic as a grammar which generates formal sentences, and then semantics being derived Boolean functions on them, by way of assignments) and a "Models of Computation" type automata-theory/language course as LTL checking relies on omega regular languages and Generalised non-deterministic Buchi automata and these are quite a bitch to get your head around if you haven't seen DFAs/NFAs. I only took my Uni's base course in FV but I looked into the second course and there's a lot about working with infinite automata.