2019/09/09 by Miguel Romero, Romero, Miguel, Sergio Ramírez +6
Computer Science · #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1909.03819
openalex publication_date 2019/09/09 · openalex created_date 2022/11/09 · openalex updated_date 2026/07/28
This paper addresses the issue of specifying, simulating, and verifying\nreactive systems in rewriting logic. It presents an executable semantics for\nprobabilistic, timed, and spatial concurrent constraint programming -- here\ncalled stochastic and spatial concurrent constraint systems (SSCC) -- in the\nrewriting logic semantic framework. The approach is based on an enhanced and\ngeneralized model of concurrent constraint programming (CCP) where\ncomputational hierarchical spaces can be assigned to belong to agents. The\nexecutable semantics faithfully represents and operationally captures the\nhighly concurrent nature, uncertain behavior, and spatial and epistemic\ncharacteristics of reactive systems with flow of information. In SSCC, timing\nattributes -- represented by stochastic duration -- can be associated to\nprocesses, and exclusive and independent probabilistic choice is also\nsupported. SMT solving technology, available from the Maude system, is used to\nrealize the underlying constraint system of SSCC with quantifier-free formulas\nover integers and reals. This results in a fully executable real-time symbolic\nspecification that can be used for quantitative analysis in the form of\nstatistical model checking. The main features and capabilities of SSCC are\nillustrated with examples throughout the paper. This contribution is part of a\nlarger research effort aimed at making available formal analysis techniques and\ntools, mathematically founded on the CCP approach, to the research community.\n