Parallel and distributed systems
- Graphs and graph algorithms. Formalization of basic graph terms, representation of graphs. Chart Link, Color, Plane Charts. Algorithms (including complexity and basic idea of proof of correctness): scanning the chart to width and depth, shortest distance, skeleton, network flows.
- Mathematical Logic. Pronounced and predicate logic, syntax, semantics. Derivation systems, formal evidence. Correctness and completeness of derived systems. Gödel's theorems of incompleteness.
- Finite automata (FA) and logic over words. 1st order logic (FOL) and 2nd order monadic logic (MSOL): syntax and semantics FOL and MSOL, principles of transferability between FA and MSOL formulas. Automata over infinite words and omega-regular languages.
- Operational, denotational, and axiomatic semantics of programming languages. CPO, fixed point clause, and its use. Hora's logic, its correctness and completeness. Temporal logic of linear and branching time and their fragments, semantics of unfinished and parallel programs.
- Model Verification Method (MC) for finally state systems and linear temporal logic. The principle of LTL formula translation into automata over infinite words. Basic symbolic and explicit algorithms for MC and their theoretical complexity.
- Formalisms for modeling infinite state systems (Petri nets, process rewriting systems, automata, process calculus) and algebra of processes, comparing their expressive power with regard to bisimulation. Selected decisive problems in the verification of these systems.
- Specific techniques for verifying software systems, abstract interpretations, abstraction and approximation methods, partial arrangement reductions, abstraction refinement methods (eg CEGAR - an example controlled abstraction refinement).
- Real time systems. Soft and hard systems. Planning in real-time systems: planning with periodic tasks, priority-based planning, access to shared resources.
- Models of distributed systems - basic concepts and principles, synchronous and asynchronous communications. Synchronization. Termination detection. The problem of mutual exclusion and the problem of deadlocks and their solution. The problem of choosing a leader element - the influence of topology and its knowledge / ignorance on the complexity of solving the problem.
- Computer networks - basic concepts, principles, architecture. Connected and unbundled networks, OSI model, Internet protocols. Routing, basic computer network services, network management and security.
PA151 nebo PA159