TY - GEN
T1 - Maximal causal models for sequentially consistent systems
AU - Serbanuta, Traian Florin
AU - Chen, Feng
AU - Roşu, Grigore
N1 - Funding Information:
This work was supported in part by Contract 161/15.06.2010, SMISCSNR 602-12516 (DAK), by NSA contract H98230-10-C-0294 and by NSF grant CCF-0916893.
PY - 2013
Y1 - 2013
N2 - This paper shows that it is possible to build a maximal and sound causal model for concurrent computations from a given execution trace. It is sound, in the sense that any program which can generate a trace can also generate all traces in its causal model. It is maximal (among sound models), in the sense that by extending the causal model of an observed trace with a new trace, the model becomes unsound: there exists a program generating the original trace which cannot generate the newly introduced trace. Thus, the maximal sound model has the property that it comprises all traces which all programs that can generate the original trace can also generate. The existence of such a model is of great theoretical value as it can be used to prove the soundness of non-maximal, and thus smaller, causal models.
AB - This paper shows that it is possible to build a maximal and sound causal model for concurrent computations from a given execution trace. It is sound, in the sense that any program which can generate a trace can also generate all traces in its causal model. It is maximal (among sound models), in the sense that by extending the causal model of an observed trace with a new trace, the model becomes unsound: there exists a program generating the original trace which cannot generate the newly introduced trace. Thus, the maximal sound model has the property that it comprises all traces which all programs that can generate the original trace can also generate. The existence of such a model is of great theoretical value as it can be used to prove the soundness of non-maximal, and thus smaller, causal models.
UR - http://www.scopus.com/inward/record.url?scp=84872863719&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84872863719&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-35632-2_16
DO - 10.1007/978-3-642-35632-2_16
M3 - Conference contribution
AN - SCOPUS:84872863719
SN - 9783642356315
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 136
EP - 150
BT - Runtime Verification - Third International Conference, RV 2012, Revised Selected Papers
PB - Springer
T2 - 3rd International Conference on Runtime Verification, RV 2012
Y2 - 25 September 2012 through 28 September 2012
ER -