@inproceedings{17126, abstract = {Functional encryption (FE) is a primitive where the holder of a master secret key can control which functions a user can evaluate on encrypted data. It is a powerful primitive that even implies indistinguishability obfuscation (iO), given sufficiently compact ciphertexts (Ananth-Jain, CRYPTO’15 and Bitansky-Vaikuntanathan, FOCS’15). However, despite being extensively studied, there are FE schemes, such as function-hiding inner-product FE (Bishop-Jain-Kowalczyk, AC’15, Abdalla-Catalano-Fiore-Gay-Ursu, CRYPTO’18) and compact quadratic FE (Baltico-Catalano-Fiore-Gay, Lin, CRYPTO’17), that can be only realized using pairings. This raises the question if there are some mathematical barriers that hinder us from realizing these FE schemes from other assumptions. In this paper, we study the difficulty of constructing lattice-based compact FE. We generalize the impossibility results of Ünal (EC’20) for lattice-based function-hiding FE, and extend it to the case of compact FE. Concretely, we prove lower bounds for lattice-based compact FE schemes which meet some (natural) algebraic restrictions at encryption and decryption, and have ciphertexts of linear size and secret keys of minimal degree. We see our results as important indications of why it is hard to construct lattice-based FE schemes for new functionalities, and which mathematical barriers have to be overcome.}, author = {Tairi, Erkan and Ünal, Akin}, booktitle = {Advances in Cryptology – EUROCRYPT 2024}, isbn = {9783031587221}, issn = {1611-3349}, location = {Zurich, Switzerland}, pages = {249--279}, publisher = {Springer Nature}, title = {{Lower bounds for lattice-based compact functional encryption}}, doi = {10.1007/978-3-031-58723-8_9}, volume = {14652}, year = {2024}, } @inproceedings{18521, abstract = {In distributed systems with processes that do not share a global clock, partial synchrony is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an approximate distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.}, author = {Bonakdarpour, Borzoo and Momtaz, Anik and Nickovic, Dejan and Sarac, Naci E}, booktitle = {24th International Conference on Runtime Verification}, isbn = {9783031742330}, issn = {1611-3349}, location = {Istanbul, Turkey}, pages = {282--301}, publisher = {Springer Nature}, title = {{Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy}}, doi = {10.1007/978-3-031-74234-7_18}, volume = {15191}, year = {2024}, } @inbook{18563, abstract = {I give a personal account about the wave of new research activities that rose in the 1990s on the specification, verification, and control of real-time systems.}, author = {Henzinger, Thomas A}, booktitle = {Real Time and Such}, editor = {Graf, Susanne and Pettersson, Paul and Steffen, Bernhard}, isbn = {9783031737503}, issn = {1611-3349}, pages = {154--164}, publisher = {Springer Nature}, title = {{Reminiscences of a Real-Time Researcher}}, doi = {10.1007/978-3-031-73751-0_12}, volume = {15230}, year = {2024}, } @inproceedings{18599, abstract = {Hypernode logic can reason about the prefix relation on stutter-reduced finite traces through the stutter-reduced prefix predicate. We increase the expressiveness of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate into an explicit stutter-reduction operator and the classical prefix predicate on words. This change gives hypernode logic the ability to combine synchronous and asynchronous reasoning by explicitly stating which parts of traces can stutter. Second, we allow the use of regular expressions in formulas to reason about the structure of traces. This change enables hypernode logic to describe a mixture of trace properties and hyperproperties. We show how to translate extended hypernode logic formulas into multi-track automata, which are automata that read multiple input words. Then we describe a fully online monitoring algorithm for monitoring k-safety hyperproperties specified in the logic. We have implemented the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous versions of observational determinism, and on checking the privacy preservation by compiler optimizations.}, author = {Chalupa, Marek and Henzinger, Thomas A and Oliveira da Costa, Ana}, booktitle = {Integrated Formal Methods}, isbn = {9783031765537}, issn = {1611-3349}, pages = {151--171}, publisher = {Springer Nature}, title = {{Monitoring extended hypernode logic}}, doi = {10.1007/978-3-031-76554-4_9}, volume = {15234}, year = {2024}, } @inproceedings{18600, abstract = {The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today’s active areas and tomorrow’s challenges in tool-focused research for quantitative verification.}, author = {Andriushchenko, Roman and Bork, Alexander and Budde, Carlos E. and Češka, Milan and Grover, Kush and Hahn, Ernst Moritz and Hartmanns, Arnd and Israelsen, Bryant and Jansen, Nils and Jeppson, Joshua and Junges, Sebastian and Köhl, Maximilian A. and Könighofer, Bettina and Kretinsky, Jan and Meggendorfer, Tobias and Parker, David and Pranger, Stefan and Quatmann, Tim and Ruijters, Enno and Taylor, Landon and Volk, Matthias and Weininger, Maximilian and Zhang, Zhen}, booktitle = {TOOLympics Challenge 2023}, isbn = {9783031676949}, issn = {1611-3349}, pages = {90--146}, publisher = {Springer Nature}, title = {{Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report}}, doi = {10.1007/978-3-031-67695-6_4}, volume = {14550}, year = {2024}, } @inproceedings{18702, abstract = {In this work we prove lower bounds on the (communication) cost of maintaining a shared key among a dynamic group of users. Being “dynamic” means one can add and remove users from the group. This captures important protocols like multicast encryption (ME) and continuous group-key agreement (CGKA), which is the primitive underlying many group messaging applications. We prove our bounds in a combinatorial setting where the state of the protocol progresses in rounds. The state of the protocol in each round is captured by a set system, with each of its elements specifying a set of users who share a secret key. We show this combinatorial model implies bounds in symbolic models for ME and CGKA that capture, as building blocks, PRGs, PRFs, dual PRFs, secret sharing, and symmetric encryption in the setting of ME, and PRGs, PRFs, dual PRFs, secret sharing, public-key encryption, and key-updatable public-key encryption in the setting of CGKA. The models are related to the ones used by Micciancio and Panjwani (Eurocrypt’04) and Bienstock et al. (TCC’20) to analyze ME and CGKA, respectively. We prove – using the Bollobás’ Set Pairs Inequality – that the cost (number of uploaded ciphertexts) for replacing a set of d users in a group of size n is Ω(dln(n/d)). Our lower bound is asymptotically tight and both improves on a bound of Ω(d) by Bienstock et al. (TCC’20), and generalizes a result by Micciancio and Panjwani (Eurocrypt’04), who proved a lower bound of Ω(log(n)) for d=1. }, author = {Anastos, Michael and Auerbach, Benedikt and Baig, Mirza Ahad and Cueto Noval, Miguel and Kwan, Matthew Alan and Pascual Perez, Guillermo and Pietrzak, Krzysztof Z}, booktitle = {22nd International Conference on Theory of Cryptography}, isbn = {9783031780103}, issn = {1611-3349}, location = {Milan, Italy}, pages = {413--443}, publisher = {Springer Nature}, title = {{The cost of maintaining keys in dynamic groups with applications to multicast encryption and group messaging}}, doi = {10.1007/978-3-031-78011-0_14}, volume = {15364}, year = {2024}, } @inproceedings{18755, abstract = {A universalthresholdizer (UT), constructed from a threshold fully homomorphic encryption by Boneh et. al , Crypto 2018, is a general framework for universally thresholdizing many cryptographic schemes. However, their framework is insufficient to construct strongly secure threshold schemes, such as threshold signatures and threshold public-key encryption, etc. In this paper, we strengthen the security definition for a universal thresholdizer and propose a scheme which satisfies our stronger security notion. Our UT scheme is an improvement of Boneh et. al ’s construction at the level of threshold fully homomorphic encryption using a key homomorphic pseudorandom function. We apply our strongly secure UT scheme to construct strongly secure threshold signatures and threshold public-key encryption.}, author = {Ebrahimi, Ehsan and Yadav, Anshu}, booktitle = {30th International Conference on the Theory and Application of Cryptology and Information Security}, isbn = {9789819608904}, issn = {1611-3349}, location = {Kolkata, India}, pages = {207--239}, publisher = {Springer Nature}, title = {{Strongly secure universal thresholdizer}}, doi = {10.1007/978-981-96-0891-1_7}, volume = {15486}, year = {2024}, } @inproceedings{18756, abstract = {The evasive LWE assumption, proposed by Wee [Eurocrypt’22 Wee] for constructing a lattice-based optimal broadcast encryption, has shown to be a powerful assumption, adopted by subsequent works to construct advanced primitives ranging from ABE variants to obfuscation for null circuits. However, a closer look reveals significant differences among the precise assumption statements involved in different works, leading to the fundamental question of how these assumptions compare to each other. In this work, we initiate a more systematic study on evasive LWE assumptions: (i) Based on the standard LWE assumption, we construct simple counterexamples against three private-coin evasive LWE variants, used in [Crypto’22 Tsabary, Asiacrypt’22 VWW, Crypto’23 ARYY] respectively, showing that these assumptions are unlikely to hold. (ii) Based on existing evasive LWE variants and our counterexamples, we propose and define three classes of plausible evasive LWE assumptions, suitably capturing all existing variants for which we are not aware of non-obfuscation-based counterexamples. (iii) We show that under our assumption formulations, the security proofs of [Asiacrypt’22 VWW] and [Crypto’23 ARYY] can be recovered, and we reason why the security proof of [Crypto’22 Tsabary] is also plausibly repairable using an appropriate evasive LWE assumption.}, author = {Brzuska, Chris and Ünal, Akin and Woo, Ivy K.Y.}, booktitle = {30th International Conference on the Theory and Application of Cryptology and Information Security}, isbn = {9789819608935}, issn = {1611-3349}, location = {Kolkata, India}, pages = {418--449}, publisher = {Springer Nature}, title = {{Evasive LWE assumptions: Definitions, classes, and counterexamples}}, doi = {10.1007/978-981-96-0894-2_14}, volume = {15487}, year = {2024}, } @inproceedings{17402, abstract = {We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.}, author = {Meggendorfer, Tobias and Weininger, Maximilian}, booktitle = {36th International Conference on Computer Aided Verification}, isbn = {9783031656323}, issn = {1611-3349}, location = {Montreal, Canada}, pages = {359--372}, publisher = {Springer Nature}, title = {{Playing games with your PET: Extending the Partial Exploration Tool to stochastic games}}, doi = {10.1007/978-3-031-65633-0_16}, volume = {14683}, year = {2024}, } @inproceedings{17413, abstract = {Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.}, author = {Froleyks, Nils and Yu, Zhengqi and Biere, Armin and Heljanko, Keijo}, booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, isbn = {9783031634970}, issn = {1611-3349}, location = {Nancy, France}, pages = {284--303}, publisher = {Springer Nature}, title = {{Certifying phase abstraction}}, doi = {10.1007/978-3-031-63498-7_17}, volume = {14739}, year = {2024}, } @inproceedings{18086, abstract = {Abstract. Continuous group key agreement (CGKA) allows a group of users to maintain a continuously updated shared key in an asynchronous setting where parties only come online sporadically and their messages are relayed by an untrusted server. CGKA captures the basic primitive underlying group messaging schemes. Current solutions including TreeKEM (“Messaging Layer Security” (MLS) IETF RFC 9420) cannot handle concurrent requests while retaining low communication complexity. The exception being CoCoA, which is concurrent while having extremely low communication complexity (in groups of size n and for m concurrent updates the communication per user is log(n), i.e., independent of m). The main downside of CoCoA is that in groups of size n, users might have to do up to log(n) update requests to the server to ensure their (potentially corrupted) key material has been refreshed. In this work we present a “fast healing” concurrent CGKA protocol, named DeCAF, where users will heal after at most log(t) requests, with t being the number of corrupted users. While also suitable for the standard central-server setting, our protocol is particularly interesting for realizing decentralized group messaging, where protocol messages (add, remove, update) are being posted on some append-only data structure rather than sent to a server. In this setting, concurrency is crucial once the rate of requests exceeds, say, the rate at which new blocks are added to a blockchain. In the central-server setting, CoCoA (the only alternative with concurrency, sub-linear communication and basic post-compromise security) enjoys much lower download communication. However, in the decentralized setting – where there is no server which can craft specific messages for different users to reduce their download communication – our protocol significantly outperforms CoCoA. DeCAF heals in fewer epochs (log(t) vs. log(n)) while incurring a similar per epoch per user communication cost.}, author = {Alwen, Joel F and Auerbach, Benedikt and Cueto Noval, Miguel and Klein, Karen and Pascual Perez, Guillermo and Pietrzak, Krzysztof Z}, booktitle = {Security and Cryptography for Networks: 14th International Conference}, editor = {Galdi, Clemente and Phan, Duong Hieu}, isbn = {9783031710728}, issn = {1611-3349}, location = {Amalfi, Italy}, pages = {294–313}, publisher = {Springer Nature}, title = {{DeCAF: Decentralizable CGKA with fast healing}}, doi = {10.1007/978-3-031-71073-5_14}, volume = {14974}, year = {2024}, } @inproceedings{18155, abstract = {We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.}, author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Goharshady, Ehsan and Karrabi, Mehrdad and Zikelic, Dorde}, booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, isbn = {9783031711619}, issn = {1611-3349}, location = {Milan, Italy}, pages = {600--619}, publisher = {Springer Nature}, title = {{Sound and complete witnesses for template-based verification of LTL properties on polynomial programs}}, doi = {10.1007/978-3-031-71162-6_31}, volume = {14933}, year = {2024}, } @inproceedings{18177, abstract = {Partially Specified Boolean Networks (PSBNs) represent a family of Boolean models resulting from possible interpretations of unknown update logics. Hybrid extension of CTL (HCTL) has the power to express complex dynamical phenomena, such as oscillations or stability. We present BNClassifier to classify Boolean Networks corresponding to a given PSBN according to criteria specified in HCTL. The implementation of the tool is fully symbolic (based on BDDs). The results are visualised using the machine-learning-based technology of decision trees.}, author = {Beneš, Nikola and Brim, Luboš and Huvar, Ondřej and Pastva, Samuel and Šafránek, David}, booktitle = {Computational Methods in Systems Biology}, isbn = {9783031716706}, issn = {1611-3349}, pages = {19--26}, publisher = {Springer Nature}, title = {{BNClassifier: Classifying boolean models by dynamic properties}}, doi = {10.1007/978-3-031-71671-3_2}, volume = {14971}, year = {2024}, } @inproceedings{18206, abstract = {In the context of in vitro fertilization (IVF), selecting embryos for transfer is critical in determining pregnancy outcomes, with implantation as the essential first milestone for a successful pregnancy. This study introduces the Bonna algorithm, an advanced deep-learning framework engineered to predict embryo implantation probabilities. The algorithm employs a sophisticated integration of machine-learning techniques, utilizing MobileNetV2 for pixel and context embedding, a custom Pix2Pix model for precise segmentation, and a Vision Transformer for additional depth in embedding. MobileNetV2 was chosen for its robust feature extraction capabilities, focusing on textures and edges. The custom Pix2Pix model is adapted for precise segmentation of significant biological features such as the zona pellucida and blastocyst cavity. The Vision Transformer adds a global perspective, capturing complex patterns not apparent in local image segments. Tested on a dataset of images of human blastocysts collected from Ukraine, Israel, and Spain, the Bonna algorithm was rigorously validated through 10-fold cross-validation to ensure its robustness and reliability. It demonstrates superior performance with a mean area under the receiver operating characteristic curve (AUC) of 0.754, significantly outperforming existing models. The study not only advances predictive accuracy in embryo selection but also highlights the algorithm’s clinical applicability due to reliable confidence reporting.}, author = {Rave, Gilad and Fordham, Daniel E. and Bronstein, Alexander and Silver, David H.}, booktitle = {First International Conference on Artificial Intelligence in Healthcare}, isbn = {9783031672842}, issn = {1611-3349}, location = {Swansea, United Kingdom}, pages = {160--171}, publisher = {Springer Nature}, title = {{Enhancing predictive accuracy in embryo implantation: The Bonna algorithm and its clinical implications}}, doi = {10.1007/978-3-031-67285-9_12}, volume = {14976}, year = {2024}, } @inproceedings{17634, abstract = {System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and executions. Quantitative automata offer a more nuanced approach, mapping each execution to a real number by incorporating weighted transitions and value functions generalizing acceptance conditions. In this paper, we introduce QuAK, the first tool designed to automate the analysis of quantitative automata. QuAK currently supports a variety of quantitative automaton types, including Inf, Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision procedures for problems such as emptiness, universality, inclusion, equivalence, as well as for checking whether an automaton is safe, live, or constant. Additionally, QuAK is able to compute extremal values when possible, construct safety-liveness decompositions, and monitor system behaviors. We demonstrate the effectiveness of QuAK through experiments focusing on the inclusion, constant-function check, and monitoring problems.}, author = {Chalupa, Marek and Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E}, booktitle = {12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation}, isbn = {9783031753862}, issn = {1611-3349}, location = {Crete, Greece}, pages = {3--20}, publisher = {Springer Nature}, title = {{QuAK: Quantitative Automata Kit}}, doi = {10.1007/978-3-031-75387-9_1}, volume = {15222}, year = {2024}, } @inproceedings{12467, abstract = {Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). In quantitative specification and verification, properties assign not truth values, but quantitative values to infinite traces (e.g., a cost, or the distance to a boolean property). We introduce quantitative safety and liveness, and we prove that our definitions induce conservative quantitative generalizations of both (1)~the safety-progress hierarchy of boolean properties and (2)~the safety-liveness decomposition of boolean properties. In particular, we show that every quantitative property can be written as the pointwise minimum of a quantitative safety property and a quantitative liveness property. Consequently, like boolean properties, also quantitative properties can be min-decomposed into safety and liveness parts, or alternatively, max-decomposed into co-safety and co-liveness parts. Moreover, quantitative properties can be approximated naturally. We prove that every quantitative property that has both safe and co-safe approximations can be monitored arbitrarily precisely by a monitor that uses only a finite number of states.}, author = {Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E}, booktitle = {26th International Conference Foundations of Software Science and Computation Structures}, isbn = {9783031308284}, issn = {1611-3349}, location = {Paris, France}, pages = {349--370}, publisher = {Springer Nature}, title = {{Quantitative safety and liveness}}, doi = {10.1007/978-3-031-30829-1_17}, volume = {13992}, year = {2023}, } @inproceedings{12854, abstract = {The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis. At SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.}, author = {Chalupa, Marek and Henzinger, Thomas A}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031308192}, issn = {1611-3349}, location = {Paris, France}, pages = {535--540}, publisher = {Springer Nature}, title = {{Bubaak: Runtime monitoring of program verifiers}}, doi = {10.1007/978-3-031-30820-8_32}, volume = {13994}, year = {2023}, } @inproceedings{12856, abstract = {As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both. We present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems. We implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.}, author = {Chalupa, Marek and Mühlböck, Fabian and Muroya Lei, Stefanie and Henzinger, Thomas A}, booktitle = {Fundamental Approaches to Software Engineering}, isbn = {9783031308253}, issn = {1611-3349}, location = {Paris, France}, pages = {260--281}, publisher = {Springer Nature}, title = {{Vamos: Middleware for best-effort third-party monitoring}}, doi = {10.1007/978-3-031-30826-0_15}, volume = {13991}, year = {2023}, } @inproceedings{13139, abstract = {A classical problem for Markov chains is determining their stationary (or steady-state) distribution. This problem has an equally classical solution based on eigenvectors and linear equation systems. However, this approach does not scale to large instances, and iterative solutions are desirable. It turns out that a naive approach, as used by current model checkers, may yield completely wrong results. We present a new approach, which utilizes recent advances in partial exploration and mean payoff computation to obtain a correct, converging approximation.}, author = {Meggendorfer, Tobias}, booktitle = {TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031308222}, issn = {1611-3349}, location = {Paris, France}, pages = {489--507}, publisher = {Springer Nature}, title = {{Correct approximation of stationary distributions}}, doi = {10.1007/978-3-031-30823-9_25}, volume = {13993}, year = {2023}, } @inproceedings{13141, abstract = {We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an ω-regular winning condition Φ for the system player, we compute an ω-regular assumption Ψ for the environment player, such that (i) every environment strategy compliant with Ψ allows the system to fulfill Φ (sufficiency), (ii) Ψ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) Ψ does not prevent any cooperative strategy choice (permissiveness). For parity games, which are canonical representations of ω-regular games, we present a polynomial-time algorithm for the symbolic computation of adequately permissive assumptions and show that our algorithm runs faster and produces better assumptions than existing approaches—both theoretically and empirically. To the best of our knowledge, for ω -regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.}, author = {Anand, Ashwani and Mallik, Kaushik and Nayak, Satya Prakash and Schmuck, Anne Kathrin}, booktitle = {TACAS 2023: Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031308192}, issn = {1611-3349}, location = {Paris, France}, pages = {211--228}, publisher = {Springer Nature}, title = {{Computing adequately permissive assumptions for synthesis}}, doi = {10.1007/978-3-031-30820-8_15}, volume = {13994}, year = {2023}, }