ACTA INFORMATICA信息学报
ACTA INFORMATICA(英文缩写 ACTA INFORM),ISSN 0001-5903,eISSN 1432-0525,中文译名:信息学报 是一本学术期刊。本页汇总该期刊的最新影响因子、分区信息以及最新收录于 PubMed 的文献,帮助您快速了解期刊全貌。
发文量统计区间：2025-11-01 至 2026-10-31，按本站收录文献的发表日期统计。
期刊介绍
历年影响因子趋势
| JCR 数据年份 | 影响因子 | JCR 分区 |
|---|---|---|
| 2021 | 0.871 | Q4 |
| 2022 | 0.600 | Q4 |
| 2023 | 0.400 | Q4 |
| 2024 | 0.500 | Q4 |
| 2025 | 1.200 | Q4 |
ACTA INFORMATICA 最新收录文献
-
1. A natural deduction system for the Byzantine Generals Oral Messages algorithm.
PMID:日期:2026-06-16The Oral Messages algorithm OM() is an algorithm that uses message relay rounds to solve the Byzantine Generals Problem [5]. It is a landmark result, however its original specification is informal and its correctness proof sketchy, making both hard to understand. The proof is rewritten here using a natural deduction system formulated directly from the message flows described for OM() in [5]. The system comprises only two inference rules which can be used to explain the original algorithm via derivations. The rules are shown complete relative to OM() and sound in the sense they cannot be used to derive consensus when it is impossible [8]. The completeness proof provides more details than the original correctness proof, clearly showing the role of , the risk it creates, and why the algorithm succeeds under well-known constraints.
-
2. Exact and parameterized algorithms for choosability.
PMID:日期:2025-05-30In the Choosability problem (or list chromatic number problem), for a given graph , we need to find the smallest such that admits a list coloring for any list assignment where all lists contain at least colors. The problem is tightly connected with the well-studied Coloring and List Coloring problems. However, the knowledge of the complexity landscape for the Choosability problem is pretty scarce. Moreover, most of the known results only provide lower bounds for its computational complexity and do not provide ways to cope with the intractability. The main objective of our paper is to construct the first non-trivial exact exponential algorithms for the Choosability problem, and complete the picture with parameterized results. Specifically, we present the first single-exponential algorithm for the decision version of the problem with fixed . This result answers an implicit question from Eppstein on a stackexchange thread discussing upper bounds on the union of lists assigned to vertices. We also present a [Formula: see text] time algorithm for the general Choosability problem. In the parameterized setting, we give a polynomial kernel for the problem parameterized by vertex cover, and algorithms that run in FPT time when parameterized by a size of a clique-modulator and by the dual parameterization [Formula: see text]. Additionally, we show that Choosability admits a significant running time improvement if it is parameterized by cutwidth in comparison with the parameterization by treewidth studied by Marx and Mitsou [ICALP'16]. On the negative side, we provide a lower bound parameterized by a size of a modulator to split graphs under assumption of the Exponential Time Hypothesis.
-
3. Reoptimization of parameterized problems.
PMID:日期:2022-07-25Parameterized complexity allows us to analyze the time complexity of problems with respect to a natural parameter depending on the problem. Reoptimization looks for solutions or approximations for problem instances when given solutions to neighboring instances. We combine both techniques, in order to better classify the complexity of problems in the parameterized setting. Specifically, we see that some problems in the class of compositional problems, which do not have polynomial kernels under standard complexity-theoretic assumptions, do have polynomial kernels under the reoptimization model for some local modifications. We also observe that, for some other local modifications, these same problems do not have polynomial kernels unless . We find examples of compositional problems, whose reoptimization versions do not have polynomial kernels under any of the considered local modifications. Finally, in another negative result, we prove that the reoptimization version of Connected Vertex Cover does not have a polynomial kernel unless Set Cover has a polynomial compression. In a different direction, looking at problems with polynomial kernels, we find that the reoptimization version of Vertex Cover has a polynomial kernel of size using crown decompositions only, which improves the size of the kernel achievable with this technique in the classic problem.
-
4. Indecision and delays are the parents of failure-taming them algorithmically by synthesizing delay-resilient control.
PMID:日期:2020-02-20The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing and actuating the environment through physical devices nor data forwarding to and from the controller and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play and to submit these decisions well before they can take effect asynchronously. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to -regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm successively synthesizing a series of controllers handling increasing delays and reducing the game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore address the practically relevant cases of non-order-preserving delays and bounded message loss, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay.
-
5. Synthesis from hyperproperties.
PMID:日期:2019-12-07We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to of traces. Typical examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal logics like LTL, CTL, or . Furthermore, HyperLTL subsumes many classical extensions of the LTL realizability problem, including realizability under incomplete information, distributed synthesis, and fault-tolerant synthesis. We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the , , and the fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL, we present a semi-decision procedure that constructs implementations and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy, and information flow.
-
6. Automated formal synthesis of provably safe digital controllers for continuous plants.
PMID:日期:2019-12-06We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as time-invariant models. Models are linear differential equations with inputs, evolving over a continuous state space. The synthesis precisely accounts for the effects of finite-precision arithmetic introduced by the controller. The approach uses counterexample-guided inductive synthesis: an inductive generalization phase produces a controller that is known to stabilize the model but that may not be safe for all initial conditions of the model. Safety is then verified via bounded model checking: if the verification step fails, a counterexample is provided to the inductive generalization, and the process further iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for physical plant models from the digital control literature.
-
7. Performance heuristics for GR(1) synthesis and related algorithms.
PMID:日期:2019-12-05Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this work we present and evaluate a list of heuristics to potentially reduce running times for GR(1) synthesis and related algorithms. The list includes several heuristics for controlled predecessor computation and BDDs, early detection of fixed-points and unrealizability, fixed-point recycling, and several heuristics for unrealizable core computations. We have implemented the heuristics and integrated them in our synthesis environment Spectra Tools, a set of tools for writing specifications and running synthesis and related analyses. We evaluate the presented heuristics on SYNTECH15, a total of 78 specifications of 6 autonomous Lego robots, on SYNTECH17, a total of 149 specifications of 5 autonomous Lego robots, all written by 3rd year undergraduate computer science students in two project classes we have taught, as well as on benchmarks from the literature. The evaluation investigates not only the potential of the suggested heuristics to improve computation times, but also the difference between existing benchmarks and the robot's specifications in terms of the effectiveness of the heuristics. Our evaluation shows positive results for the application of all the heuristics together, which get more significant for specifications with slower original running times. It also shows differences in effectiveness when applied to different sets of specifications. Furthermore, a comparison between Spectra, with all the presented heuristics, and two existing tools, RATSY and Slugs, over two well-known benchmarks, shows that Spectra outperforms both on most of the specifications; the larger the specification, the faster Spectra becomes relative to the two other tools.
-
8. Distributive laws for monotone specifications.
8. 单调规格的分配律PMID:日期:2019-02-22Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that specifications-that disallow negative premises-do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation.
-
9. Characteristic bisimulation for higher-order session processes.
PMID:日期:2016-12-24For higher-order (process) languages, characterising contextual equivalence is a long-standing issue. In the setting of a higher-order -calculus with , we develop , a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.
-
10. Compositional schedulability analysis of real-time actor-based systems.
10. 基于角色的实时系统组合可调度性分析PMID:日期:2016-01-25We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,"earliest deadline first" which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker.