This data deposit consists of a directory containing models and properties for use with the Prism model-checker. The directory has been archived and compressed using tar and gzip. When uncompressed it contains a selection of .pm and .pctl files. The .pm files are Prism models and the .pctl files are properties. Model Files =========== The model files are paper_example1.pm paper_example2.pm paper_example3.pm paper_example4.pm paper_example5.pm Each file refers to a model discussed in the paper "How Did They Know?" - Model-Checking for Analysis of Information Leakage in Social Networks’ that appears in the COIN@ECAI 2016 proceedings volume. The files are named in order to refer to the relevant model in the paper - i.e., paper_example1.pm refers to the model discussed in Example 1 in the paper. Property files ============== The property files contain the following properties. property_alice_message.pctl - P=? [F(alice_has_message = true)] - what is the probability that eventually alice_has_message property_charlie_message.pctl - P=? [F(charlie_has_message = true)] - what is the probability that eventually charlie_has_message property_debbie_message.pctl - P=? [F(debbie_has_message = true)] - what is the probability that eventually debbie_has_message property_sync_message.pctl - P=? [F(sync_has_message = true)] - what is the probability that eventually sync_has_message Usage ===== The paper discusses the checking of the models against the properties using the Prism model checking tool version 4.1. Prism can be downloaded from www.prismmodelchecker.org. For instance, to determine the probability that eventually alice_has_message in model paper_example1.pm one executes at the command line: > prism paper_example1.pm propert_alice_message.pctl