You can access a PLASMA Lab project library<\/strong><\/a> containing a selection of case studies and examples of various types. These project are compatible with the latest version of PLASMA Lab.<\/p>\n These uses cases have been developed for different projects, some of them using project specific simulators.<\/p>\n Here you can find several examples demonstrating the different simulators, checkers and some specific algorithms of PLASMA Lab (besides Monte-Carlo methods).<\/p>\n PLASMA Lab case studies library You can access a PLASMA Lab project library containing a selection of case studies and examples of various types. These project are compatible with the latest version of PLASMA Lab. Use cases These uses cases have been developed for different projects, some of them using\u2026<\/p>\n
\nUse cases<\/h2>\n
\n
\nExamples<\/h2>\n
\n
\n Example<\/strong><\/th>\n Simulator(s)<\/strong><\/th>\n Checker(s)<\/strong><\/th>\n Algorithm(s)<\/strong><\/th>\n<\/tr>\n \n Dining philosophers<\/a><\/td>\n RML (DTMC)<\/td>\n BLTL
\nObserver<\/td>\nImportance splitting<\/td>\n<\/tr>\n \n Probabilistic Broadcast protocols<\/a><\/td>\n RML (DTMC)<\/td>\n BLTL<\/td>\n <\/td>\n<\/tr>\n \n Synchronous Leader Election Protocol<\/a><\/td>\n RML (DTMC)<\/td>\n BLTL<\/td>\n <\/td>\n<\/tr>\n \n Hubble<\/a><\/td>\n RML (CTMC)<\/td>\n BLTL<\/td>\n <\/td>\n<\/tr>\n \n Chemical<\/a><\/td>\n Bio<\/td>\n BLTL<\/td>\n <\/td>\n<\/tr>\n \n Genetic oscillator<\/a><\/td>\n RML (CTMC), Bio<\/td>\n BLTL<\/td>\n <\/td>\n<\/tr>\n \n IEEE 802.11 wireless LAN<\/a><\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs<\/td>\n<\/tr>\n \n IEEE 802.3 CSMA\/CD<\/a><\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs<\/td>\n<\/tr>\n \n Network virus infection<\/a><\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs
\nReward estimation for MDPs\n<\/td>\n<\/tr>\n\n Gossip protocol<\/a> <\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs
\nReward estimation for MDPs\n<\/td>\n<\/tr>\n\n Choice coordination<\/a> <\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs
\nReward estimation for MDPs\n<\/td>\n<\/tr>\n\n Self-stabilisation<\/a> <\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs
\nReward estimation for MDPs\n<\/td>\n<\/tr>\n\n Randomised Consensus Shared Coin Protocol<\/a><\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n Probability estimation for MDPs
\nReward estimation for MDPs\n<\/td>\n<\/tr>\n\n Process partitioning<\/a><\/td>\n RML (MDP)<\/td>\n BLTL<\/td>\n<\/tr>\n \n Simple chain <\/a><\/td>\n RML (DTMC)<\/td>\n Observer<\/td>\n Importance splitting<\/td>\n<\/tr>\n<\/table>\n","protected":false},"excerpt":{"rendered":"