We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Program Repair for Hyperproperties

Abstract: We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class of properties includes information flow policies like noninterference and observational determinism. The repair problem is to find, for a given Kripke structure, a substructure that satisfies a given specification. We show that the repair problem is decidable for HyperLTL specifications and finite-state Kripke structures. We provide a detailed complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures.
Comments: arXiv admin note: text overlap with arXiv:2101.07847
Subjects: Logic in Computer Science (cs.LO)
DOI: 10.1007/978-3-030-31784-3_25
Cite as: arXiv:2101.08257 [cs.LO]
  (or arXiv:2101.08257v1 [cs.LO] for this version)

Submission history

From: Bernd Finkbeiner [view email]
[v1] Tue, 19 Jan 2021 20:21:36 GMT (112kb)

Link back to: arXiv, form interface, contact.