Lower complexity bounds in justification logic

Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are $\Pi^p_2$-hard, reproving and generalizing an earlier result by Milnikel.

Closed-loop control of mean arterial blood pressure during surgery with alfentanil: clinical evaluation of a novel model-based predictive controller

BACKGROUND: In contrast to hypnosis, there is no surrogate parameter for analgesia in anesthetized patients. Opioids are titrated to suppress blood pressure response to noxious stimulation. The authors evaluated a novel model predictive controller for closed-loop administration of alfentanil using mean arterial blood pressure and predicted plasma alfentanil concentration (Cp Alf) as input parameters. METHODS: The authors studied 13 healthy patients scheduled to undergo minor lumbar and cervical spine surgery. After induction with propofol, alfentanil, and mivacurium and tracheal intubation, isoflurane was titrated to maintain the Bispectral Index at 55 (+/- 5), and the alfentanil administration was switched from manual to closed-loop control. The controller adjusted the alfentanil infusion rate to maintain the mean arterial blood pressure near the set-point (70 mmHg) while minimizing the Cp Alf toward the set-point plasma alfentanil concentration (Cp Alfref) (100 ng/ml). RESULTS: Two patients were excluded because of loss of arterial pressure signal and protocol violation. The alfentanil infusion was closed-loop controlled for a mean (SD) of 98.9 (1.5)% of presurgery time and 95.5 (4.3)% of surgery time. The mean (SD) end-tidal isoflurane concentrations were 0.78 (0.1) and 0.86 (0.1) vol%, the Cp Alf values were 122 (35) and 181 (58) ng/ml, and the Bispectral Index values were 51 (9) and 52 (4) before surgery and during surgery, respectively. The mean (SD) absolute deviations of mean arterial blood pressure were 7.6 (2.6) and 10.0 (4.2) mmHg (P = 0.262), and the median performance error, median absolute performance error, and wobble were 4.2 (6.2) and 8.8 (9.4)% (P = 0.002), 7.9 (3.8) and 11.8 (6.3)% (P = 0.129), and 14.5 (8.4) and 5.7 (1.2)% (P = 0.002) before surgery and during surgery, respectively. A post hoc simulation showed that the Cp Alfref decreased the predicted Cp Alf compared with mean arterial blood pressure alone. CONCLUSION: The authors' controller has a similar set-point precision as previous hypnotic controllers and provides adequate alfentanil dosing during surgery. It may help to standardize opioid dosing in research and may be a further step toward a multiple input-multiple output controller.

Object-Oriented Legacy System Trace-based Logic Testing

When reengineering legacy systems, it is crucial to assess if the legacy behavior has been preserved or how it changed due to the reengineering effort. Ideally if a legacy system is covered by tests, running the tests on the new version can identify potential differences or discrepancies. However, writing tests for an unknown and large system is difficult due to the lack of internal knowledge. It is especially difficult to bring the system to an appropriate state. Our solution is based on the acknowledgment that one of the few trustable piece of information available when approaching a legacy system is the running system itself. Our approach reifies the execution traces and uses logic programming to express tests on them. Thereby it eliminates the need to programatically bring the system in a particular state, and handles the test-writer a high-level abstraction mechanism to query the trace. The resulting system, called TESTLOG, was used on several real-world case studies to validate our claims.